# HG changeset patch
# User nipkow
# Date 916069907 -3600
# Node ID 0a2798ea600c6a06f3cba65d96abbf9fe9d694fc
# Parent  4f7975c74cdfa56c62a840018736892264e9803e
More arith simplifications

diff -r 4f7975c74cdf -r 0a2798ea600c src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Mon Jan 11 16:50:49 1999 +0100
+++ b/src/HOLCF/Fix.ML	Mon Jan 11 16:51:47 1999 +0100
@@ -702,8 +702,6 @@
         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
         atac 2,
         res_inst_tac [("x","i")] exI 1,
-        Simp_tac 1,
-	strip_tac 1,
         Asm_simp_tac 1
         ]);
 
@@ -884,7 +882,6 @@
         atac 1]);
 
 val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
-        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less,
-        adm_iff];
+        adm_all2,adm_not_less,adm_not_conj,adm_iff];
 
 Addsimps adm_lemmas;