src/HOL/Isar_Examples/ROOT.ML
author haftmann
Wed Jun 30 16:46:44 2010 +0200 (2010-06-30)
changeset 37659 14cabf5fa710
parent 33026 8f35633c4922
child 37672 645eb9fec794
permissions -rw-r--r--
more speaking names
wenzelm@33026
     1
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
wenzelm@6444
     2
haftmann@32479
     3
no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"];
wenzelm@24228
     4
wenzelm@24228
     5
use_thys [
wenzelm@31758
     6
  "Basic_Logic",
wenzelm@24228
     7
  "Cantor",
wenzelm@24228
     8
  "Peirce",
wenzelm@24228
     9
  "Drinker",
wenzelm@31758
    10
  "Expr_Compiler",
wenzelm@24228
    11
  "Group",
wenzelm@24228
    12
  "Summation",
wenzelm@31758
    13
  "Knaster_Tarski",
wenzelm@31758
    14
  "Mutilated_Checkerboard",
wenzelm@24228
    15
  "Puzzle",
wenzelm@31758
    16
  "Nested_Datatype",
wenzelm@31758
    17
  "Hoare_Ex"
wenzelm@24228
    18
];