author  wenzelm 
Thu, 31 May 2007 11:00:06 +0200  
changeset 23145  5d8faadf3ecf 
parent 23144  4a9c9e260abf 
child 23158  749b6870b1a1 
permissions  rwrr 
19495  1 
(* Title: HOL/Nominal/Examples/ROOT.ML 
2 
ID: $Id$ 

3 
Author: Christian Urban, TU Muenchen 

4 

5 
Various examples involving nominal datatypes. 

6 
*) 

7 

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  11 
use_thy "Compile"; 
12 
use_thy "Fsub"; 

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  16 
use_thy "Weakening"; 
22448  17 
use_thy "Crary"; 
23144  18 
use_thy "SOS"; 
23145  19 
use_thy "LocalWeakening"; 