author | wenzelm |
Sat, 28 Jul 2007 20:40:20 +0200 | |
changeset 24018 | edd20fe274b5 |
parent 24017 | 363287741ebe |
child 24019 | 67bde7cfcf10 |
--- a/src/HOL/Bali/AxCompl.thy Sat Jul 28 20:40:19 2007 +0200 +++ b/src/HOL/Bali/AxCompl.thy Sat Jul 28 20:40:20 2007 +0200 @@ -663,9 +663,6 @@ qed qed - -ML"Addsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]" - lemma MGFn_Loop: assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"