equal
deleted
inserted
replaced
1 theory Test |
1 theory Test |
2 imports "Parser" "../Attic/Prove" |
2 imports "Parser" "../Attic/Prove" |
3 begin |
3 begin |
4 |
|
5 text {* example 1, equivalent to example 2 from Terms *} |
|
6 |
4 |
7 atom_decl name |
5 atom_decl name |
8 |
6 |
9 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
10 |
8 |
87 sorry |
85 sorry |
88 then have "P c (0 \<bullet> lm)" by blast |
86 then have "P c (0 \<bullet> lm)" by blast |
89 then show "P c lm" by simp |
87 then show "P c lm" by simp |
90 qed |
88 qed |
91 |
89 |
|
90 text {* example 1, equivalent to example 2 from Terms *} |
|
91 |
92 nominal_datatype lam = |
92 nominal_datatype lam = |
93 VAR "name" |
93 VAR "name" |
94 | APP "lam" "lam" |
94 | APP "lam" "lam" |
95 | LAM x::"name" t::"lam" bind x in t |
95 | LAM x::"name" t::"lam" bind x in t |
96 | LET bp::"bp" t::"lam" bind "bi bp" in t |
96 | LET bp::"bp" t::"lam" bind "bi bp" in t |