Session Sort_Encodings

Theories

• 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.Infinite_Set
• HOL-Library.Countable_Set
• HOL-Library.Countable_Set_Type
• Preliminaries
• TermsAndClauses
• Sig
• M
• CM
• Mono
• Mcalc
• T_G_Prelim
• Mcalc2
• Mcalc2C
• G
• T
• U
• CU
• E
• Encodings