# HG changeset patch
# User wenzelm
# Date 1185648020 -7200
# Node ID edd20fe274b510f697537b2be3f39b91de94b381
# Parent  363287741ebe23ed843d4c77e6efd09afda0bd6b
removed redundant simproc declarations;

diff -r 363287741ebe -r edd20fe274b5 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>}"