author | wenzelm |
Sun, 06 May 2012 13:22:37 +0200 | |
changeset 47871 | 861dc9184920 |
parent 46582 | dcc312f22ee8 |
permissions | -rw-r--r-- |
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"]; use_thys [ "Basic_Logic", "Cantor", "Drinker", "Expr_Compiler", "Fibonacci", "Group", "Group_Context", "Group_Notepad", "Hoare_Ex", "Knaster_Tarski", "Mutilated_Checkerboard", "Nested_Datatype", "Peirce", "Puzzle", "Summation" ];