215 Isabelle/Pure (see \verb,Syntax.quote_tr, and |
215 Isabelle/Pure (see \verb,Syntax.quote_tr, and |
216 \verb,Syntax.quote_tr',). |
216 \verb,Syntax.quote_tr',). |
217 *} |
217 *} |
218 |
218 |
219 syntax |
219 syntax |
220 "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000) |
220 "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000) |
221 "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000) |
221 "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000) |
222 "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp" ("_[_'/\<acute>_]" [1000] 999) |
222 "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp" |
223 "_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000) |
223 ("_[_'/\<acute>_]" [1000] 999) |
224 "_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
224 "_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000) |
|
225 "_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
225 "_Cond" :: "'a bexp => 'a com => 'a com => 'a com" |
226 "_Cond" :: "'a bexp => 'a com => 'a com => 'a com" |
226 ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
227 ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
227 "_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com" |
228 "_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com" |
228 ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
229 ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
229 "_While" :: "'a bexp => 'a com => 'a com" |
230 "_While" :: "'a bexp => 'a com => 'a com" |