author | urbanc |
Thu, 20 Dec 2007 01:07:21 +0100 | |
changeset 25722 | 0a104ddb72d9 |
parent 24897 | b0a93a6d6ab9 |
child 27623 | 8e9c19529a4e |
permissions | -rw-r--r-- |
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 |
||
24153 | 8 |
use_thys [ |
9 |
"CR", |
|
10 |
"CR_Takahashi", |
|
11 |
"Class", |
|
12 |
"Compile", |
|
13 |
"Fsub", |
|
14 |
"Height", |
|
15 |
"Lambda_mu", |
|
16 |
"SN", |
|
17 |
"Weakening", |
|
18 |
"Crary", |
|
19 |
"SOS", |
|
24897 | 20 |
"LocalWeakening", |
25722 | 21 |
"Support", |
22 |
"Contexts" |
|
24153 | 23 |
]; |
24895 | 24 |
|
25722 | 25 |
setmp quick_and_dirty true use_thy "VC_Condition"; |