| author | haftmann |
| Fri, 13 Mar 2009 12:29:38 +0100 | |
| changeset 30501 | 3e3238da8abb |
| parent 24228 | 9e2234f2aff1 |
| child 31758 | 3edd5f813f01 |
| permissions | -rw-r--r-- |
(* Title: HOL/Isar_examples/ROOT.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"]; use_thys [ "BasicLogic", "Cantor", "Peirce", "Drinker", "ExprCompiler", "Group", "Summation", "KnasterTarski", "MutilatedCheckerboard", "Puzzle", "NestedDatatype", "HoareEx" ];