equal
deleted
inserted
replaced
75 absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H" |
75 absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H" |
76 | wand_tr ts = raise TERM ("wand_tr", ts); |
76 | wand_tr ts = raise TERM ("wand_tr", ts); |
77 *} |
77 *} |
78 |
78 |
79 parse_translation {* |
79 parse_translation {* |
80 [(@{syntax_const "_emp"}, emp_tr), |
80 [(@{syntax_const "_emp"}, K emp_tr), |
81 (@{syntax_const "_singl"}, singl_tr), |
81 (@{syntax_const "_singl"}, K singl_tr), |
82 (@{syntax_const "_star"}, star_tr), |
82 (@{syntax_const "_star"}, K star_tr), |
83 (@{syntax_const "_wand"}, wand_tr)] |
83 (@{syntax_const "_wand"}, K wand_tr)] |
84 *} |
84 *} |
85 |
85 |
86 text{* Now it looks much better: *} |
86 text{* Now it looks much better: *} |
87 |
87 |
88 lemma "VARS H x y z w |
88 lemma "VARS H x y z w |
126 |
126 |
127 end |
127 end |
128 *} |
128 *} |
129 |
129 |
130 print_translation {* |
130 print_translation {* |
131 [(@{const_syntax is_empty}, is_empty_tr'), |
131 [(@{const_syntax is_empty}, K is_empty_tr'), |
132 (@{const_syntax singl}, singl_tr'), |
132 (@{const_syntax singl}, K singl_tr'), |
133 (@{const_syntax star}, star_tr'), |
133 (@{const_syntax star}, K star_tr'), |
134 (@{const_syntax wand}, wand_tr')] |
134 (@{const_syntax wand}, K wand_tr')] |
135 *} |
135 *} |
136 |
136 |
137 text{* Now the intermediate proof states are also readable: *} |
137 text{* Now the intermediate proof states are also readable: *} |
138 |
138 |
139 lemma "VARS H x y z w |
139 lemma "VARS H x y z w |