Session HOL-Predicate_Compile_Examples

Theories

• HOL-Library.Predicate_Compile_Alternative_Defs
• Examples
• Predicate_Compile_Tests
• HOL-Library.Predicate_Compile_Quickcheck
  • File ‹~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML›
• Predicate_Compile_Quickcheck_Examples
• Specialisation_Examples
• IMP_1
• IMP_2
• IMP_3
• IMP_4
• HOL-Library.Code_Prolog
  • File ‹~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML›
• Code_Prolog_Examples
• Context_Free_Grammar_Example
• Hotel_Example
• Hotel_Example_Prolog
• Lambda_Example
• List_Examples
• Reg_Exp_Example