removed redundant simproc declarations;
authorwenzelm
Sat, 28 Jul 2007 20:40:20 +0200
changeset 24018 edd20fe274b5
parent 24017 363287741ebe
child 24019 67bde7cfcf10
removed redundant simproc declarations;
src/HOL/Bali/AxCompl.thy
--- 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>}"