src/HOL/Nominal/Examples/ROOT.ML
author wenzelm
Thu, 31 May 2007 11:00:06 +0200
changeset 23145 5d8faadf3ecf
parent 23144 4a9c9e260abf
child 23158 749b6870b1a1
permissions -rw-r--r--
fixed use_thy "LocalWeakening";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19495
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Nominal/Examples/ROOT.ML
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     3
    Author:     Christian Urban, TU Muenchen
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     4
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     5
Various examples involving nominal datatypes.
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     6
*)
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     7
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     8
use_thy "CR";
22823
fa9ff469247f tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents: 22448
diff changeset
     9
use_thy "CR_Takahashi";
23098
11e1a67fbfe8 took out Class.thy from the compiling process until memory problems are solved
urbanc
parents: 22823
diff changeset
    10
(*use_thy "Class";*)
21086
fe9f43a1e5bd Added Compile and Height examples.
berghofe
parents: 19499
diff changeset
    11
use_thy "Compile";
fe9f43a1e5bd Added Compile and Height examples.
berghofe
parents: 19499
diff changeset
    12
use_thy "Fsub";
fe9f43a1e5bd Added Compile and Height examples.
berghofe
parents: 19499
diff changeset
    13
use_thy "Height";
19499
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
berghofe
parents: 19495
diff changeset
    14
use_thy "Lambda_mu";
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
berghofe
parents: 19495
diff changeset
    15
use_thy "SN";
19495
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
    16
use_thy "Weakening";
22448
f982e73e36de adjusted for the example file SOS.thy
urbanc
parents: 22073
diff changeset
    17
use_thy "Crary";
23144
4a9c9e260abf included new example in the compiling process
urbanc
parents: 23098
diff changeset
    18
use_thy "SOS";
23145
5d8faadf3ecf fixed use_thy "LocalWeakening";
wenzelm
parents: 23144
diff changeset
    19
use_thy "LocalWeakening";