954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Test
|
2062
65bdcc42badd
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
2 |
imports "../NewParser"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
1600
|
5 |
(* This file contains only the examples that are not supposed to work yet. *)
|
|
6 |
|
|
7 |
|
2143
871d8a5e0c67
somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
declare [[STEPS = 2]]
|
871d8a5e0c67
somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
|
1428
|
10 |
atom_decl name
|
|
11 |
|
1398
|
12 |
(* example 4 from Terms.thy *)
|
|
13 |
(* fv_eqvt does not work, we need to repaire defined permute functions
|
|
14 |
defined fv and defined alpha... *)
|
2103
|
15 |
(* lists-datastructure does not work yet *)
|
1398
|
16 |
|
2103
|
17 |
nominal_datatype trm =
|
|
18 |
Vr "name"
|
|
19 |
| Ap "trm" "trm list"
|
|
20 |
| Lm x::"name" t::"trm" bind x in t
|
2143
871d8a5e0c67
somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
|
2103
|
22 |
|
|
23 |
(*
|
1398
|
24 |
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
|
|
25 |
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
*)
|
1398
|
27 |
|
961
|
28 |
end
|
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
|
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
|