Session Goedel_HFSet_Semanticless
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Infinite_Set
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.FSet
HOL-Library.Phantom_Type
HOL-Library.Cardinality
FinFun.FinFun
Nominal2.Nominal2_Base
File ‹nominal_basics.ML›
File ‹nominal_thmdecls.ML›
File ‹nominal_permeq.ML›
File ‹nominal_library.ML›
File ‹nominal_atoms.ML›
File ‹nominal_eqvt.ML›
HOL-Library.Quotient_Syntax
HOL-Library.Quotient_Set
HOL-Library.Quotient_Product
HOL-Library.Quotient_Option
HOL-Library.Quotient_List
Nominal2.Nominal2_Abs
Nominal2.Nominal2_FCB
Nominal2.Nominal2
File ‹nominal_dt_data.ML›
File ‹nominal_dt_rawfuns.ML›
File ‹nominal_dt_alpha.ML›
File ‹nominal_dt_quot.ML›
File ‹nominal_induct.ML›
File ‹nominal_inductive.ML›
File ‹nominal_function_common.ML›
File ‹nominal_function_core.ML›
File ‹nominal_mutual.ML›
File ‹nominal_function.ML›
File ‹nominal_termination.ML›
HereditarilyFinite.HF
HereditarilyFinite.Ordinal
HereditarilyFinite.Rank
HereditarilyFinite.OrdArith
SyntaxN
Coding
Predicates
Sigma
Coding_Predicates
Pf_Predicates
II_Prelims
Pseudo_Coding
Quote
Functions
Goedel_I
Instance