src/HOL/Isar_Examples/ROOT.ML
author huffman
Tue, 02 Mar 2010 09:54:50 -0800
changeset 35512 d1ef88d7de5a
parent 33026 8f35633c4922
child 37672 645eb9fec794
permissions -rw-r--r--
remove dead code

(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)

no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"];

use_thys [
  "Basic_Logic",
  "Cantor",
  "Peirce",
  "Drinker",
  "Expr_Compiler",
  "Group",
  "Summation",
  "Knaster_Tarski",
  "Mutilated_Checkerboard",
  "Puzzle",
  "Nested_Datatype",
  "Hoare_Ex"
];