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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 32479
diff changeset
     1
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     2
46582
dcc312f22ee8 misc tuning;
wenzelm
parents: 37672
diff changeset
     3
no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"];
24228
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
     4
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
     5
use_thys [
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
     6
  "Basic_Logic",
24228
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
     7
  "Cantor",
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
     8
  "Peirce",
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
     9
  "Drinker",
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
    10
  "Expr_Compiler",
24228
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
    11
  "Group",
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
    12
  "Summation",
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
    13
  "Knaster_Tarski",
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
    14
  "Mutilated_Checkerboard",
24228
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
    15
  "Puzzle",
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
    16
  "Nested_Datatype",
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 24228
diff changeset
    17
  "Hoare_Ex"
24228
9e2234f2aff1 simultaneous use_thys;
wenzelm
parents: 19022
diff changeset
    18
];