Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
delcongs [if_weak_cong];
authorwenzelm
Fri, 20 Aug 1999 16:16:02 +0200
changeset 7309 838a7bc92d81
parent 7308 e01aab03a2a1
child 7310 298b0dcadf2e
delcongs [if_weak_cong];
src/HOLCF/IOA/Modelcheck/MuIOA.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Aug 20 15:44:29 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Aug 20 16:16:02 1999 +0200
@@ -258,11 +258,12 @@
 by (REPEAT (rtac impI 1));
 by (REPEAT (dtac eq_reflection 1));
 (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delsimps [not_iff,split_part])
+by (full_simp_tac ((simpset() delcongs [if_weak_cong]
+                              delsimps [not_iff,split_part])
 			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
                                         rename_simps @ ioa_simps @ asig_simps)) 1);
-by (full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) 1);
-by (REPEAT (if_full_simp_tac (simpset() delsimps [not_iff,split_part]) 1));
+by (full_simp_tac (Mucke_ss delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1);
+by (REPEAT (if_full_simp_tac (simpset() delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1));
 by (call_mucke_tac 1);
 (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
 by (atac 1);
isabelle