equal
deleted
inserted
replaced
1 theory Test |
1 theory Test |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
|
5 declare [[STEPS = 4]] |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 (* |
|
10 nominal_datatype trm = |
|
11 Vr "name" |
|
12 | Ap "trm" "trm" |
|
13 |
|
14 thm fv_trm_raw.simps[no_vars] |
|
15 *) |
5 (* This file contains only the examples that are not supposed to work yet. *) |
16 (* This file contains only the examples that are not supposed to work yet. *) |
6 |
17 |
7 |
18 |
8 declare [[STEPS = 2]] |
19 declare [[STEPS = 2]] |
9 |
20 |
10 atom_decl name |
|
11 |
21 |
12 (* example 4 from Terms.thy *) |
22 (* example 4 from Terms.thy *) |
13 (* fv_eqvt does not work, we need to repaire defined permute functions |
23 (* fv_eqvt does not work, we need to repaire defined permute functions |
14 defined fv and defined alpha... *) |
24 defined fv and defined alpha... *) |
15 (* lists-datastructure does not work yet *) |
25 (* lists-datastructure does not work yet *) |