src/HOL/Isar_Examples/ROOT.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46582 dcc312f22ee8
child 47871 861dc9184920
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

(* 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",
  "Peirce",
  "Drinker",
  "Expr_Compiler",
  "Group",
  "Summation",
  "Knaster_Tarski",
  "Mutilated_Checkerboard",
  "Puzzle",
  "Nested_Datatype",
  "Hoare_Ex"
];