equal
deleted
inserted
replaced
264 constdefs |
264 constdefs |
265 |
265 |
266 is_stmt :: "term \<Rightarrow> bool" |
266 is_stmt :: "term \<Rightarrow> bool" |
267 "is_stmt t \<equiv> \<exists>c. t=In1r c" |
267 "is_stmt t \<equiv> \<exists>c. t=In1r c" |
268 |
268 |
269 ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *} |
269 ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *} |
270 |
270 |
271 declare is_stmt_rews [simp] |
271 declare is_stmt_rews [simp] |
272 |
272 |
273 text {* |
273 text {* |
274 Here is some syntactic stuff to handle the injections of statements, |
274 Here is some syntactic stuff to handle the injections of statements, |