equal
deleted
inserted
replaced
292 fn _ => fn _ => fn ct => |
292 fn _ => fn _ => fn ct => |
293 (case Thm.term_of ct of |
293 (case Thm.term_of ct of |
294 (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE |
294 (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE |
295 | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *} |
295 | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *} |
296 |
296 |
297 ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *} |
297 ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *} |
298 declare evaln_AbruptIs [intro!] |
298 declare evaln_AbruptIs [intro!] |
299 |
299 |
300 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" |
300 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" |
301 proof - |
301 proof - |
302 { fix s t v s' |
302 { fix s t v s' |