Session Goedel_HFSet_Semantic

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
• Incompleteness.SyntaxN
• Incompleteness.Coding
• Incompleteness.Predicates
• Incompleteness.Sigma
• Incompleteness.Coding_Predicates
• Incompleteness.Pf_Predicates
• Incompleteness.II_Prelims
• Incompleteness.Pseudo_Coding
• Incompleteness.Quote
• Incompleteness.Functions
• Incompleteness.Goedel_I
• Instance