Session Types_To_Sets_Extension

Theories

• ETTS_Tools
  • File ‹More_Library.ML›
  • File ‹More_Logic.ML›
  • File ‹More_Tactical.ML›
  • File ‹More_Simplifier.ML›
  • File ‹More_HOLogic.ML›
  • File ‹More_Transfer.ML›
  • File ‹ETTS_Writer.ML›
• HOL-Types_To_Sets.Types_To_Sets
  • File ‹local_typedef.ML›
  • File ‹unoverloading.ML›
  • File ‹internalize_sort.ML›
  • File ‹unoverload_type.ML›
  • File ‹unoverload_def.ML›
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• ETTS
  • File ‹ETTS_Tactics.ML›
  • File ‹ETTS_Utilities.ML›
  • File ‹ETTS_RI.ML›
  • File ‹ETTS_Substitution.ML›
  • File ‹ETTS_Context.ML›
  • File ‹ETTS_Algorithm.ML›
  • File ‹ETTS_Active.ML›
  • File ‹ETTS_Lemma.ML›
  • File ‹ETTS_Lemmas.ML›
• ETTS_Auxiliary
• Manual_Prerequisites
  • File ‹~~/src/Doc/antiquote_setup.ML›
• ETTS_Tests
  • File ‹ETTS_TEST_AMEND_CTXT_DATA.ML›
  • File ‹ETTS_TEST_TTS_ALGORITHM.ML›
  • File ‹ETTS_TEST_TTS_REGISTER_SBTS.ML›
• ETTS_Introduction
• ETTS_Theory
• ETTS_Syntax
• ETTS_Examples
• ETTS_CR
• Introduction
• SML_Introduction
• Set_Ext
• Lifting_Set_Ext
• Product_Type_Ext
• Transfer_Ext
• SML_Relations
• SML_Simple_Orders
• SML_Semigroups
• SML_Monoids
• SML_Groups
• SML_Semirings
• SML_Rings
• SML_Semilattices
• SML_Lattices
• SML_Complete_Lattices
• SML_Linorders
• 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.Set_Idioms
• HOL-Library.FuncSet
• HOL-Library.Disjoint_Sets
• HOL-Library.Product_Plus
• HOL-Analysis.Product_Vector
• HOL-Analysis.Elementary_Topology
• SML_Topological_Space
• SML_Topological_Space_Countability
• SML_Ordered_Topological_Spaces
• SML_Product_Topology
• SML_Conclusions
• VS_Prerequisites
• VS_Groups
• VS_Modules
• VS_Vector_Spaces
• VS_Conclusions
• FNDS_Introduction
• FNDS_Set_Ext
• FNDS_Definite_Description
• FNDS_Auxiliary
• Type_Simple_Orders
• Set_Simple_Orders
• Type_Semigroups
• FNDS_Lifting_Set_Ext
• Set_Semigroups
• FNDS_Conclusions