# HG changeset patch
# User paulson
# Date 931434287 -7200
# Node ID 63c9df6b5c4b077d150b21275a42f3c7a472adcb
# Parent  eba301caceea73f9262d68fd1f298060c03d55ff
Now if_weak_cong is a standard congruence rule

diff -r eba301caceea -r 63c9df6b5c4b src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Thu Jul 08 13:43:42 1999 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Thu Jul 08 13:44:47 1999 +0200
@@ -22,7 +22,7 @@
 \                   in if pre=[] then ([],xs) \
 \                      else let (xss,zs) = chop splitf post \
 \                             in (pre#xss,zs))";
-by (asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
+by (asm_simp_tac (simpset() addsimps [chopr_rule]) 1);
 by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
 qed "chop_rule";
 
@@ -35,8 +35,7 @@
 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
 by (res_inst_tac [("xs","xs")] length_induct 1);
 by (asm_simp_tac (simpset() delsplits [split_if]
-                           addsimps [chop_rule,is_maxsplitter_reducing]
-                           addcongs [if_weak_cong]) 1);
+                           addsimps [chop_rule,is_maxsplitter_reducing]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
                                 addsplits [split_split]) 1);
 qed_spec_mp "chop_concat";
@@ -44,12 +43,11 @@
 Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
 by (res_inst_tac [("xs","xs")] length_induct 1);
-by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
-                           addcongs [if_weak_cong]) 1);
+by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
-                                addsplits [split_split]) 1);
+                                 addsplits [split_split]) 1);
 by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
-                       addsplits [split_split]) 1);
+                        addsplits [split_split]) 1);
 by (etac thin_rl 1);
 by (strip_tac 1);
 by (rtac ballI 1);
diff -r eba301caceea -r 63c9df6b5c4b src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Thu Jul 08 13:43:42 1999 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Thu Jul 08 13:44:47 1999 +0200
@@ -56,8 +56,7 @@
 3) renname_ss unfolds transitions and the abstract channel *)
 
 
-val ss = (simpset() addcongs [if_weak_cong]
-                   addsimps transitions);     
+val ss = (simpset() addsimps transitions);     
 val rename_ss = (ss addsimps unfold_renaming);
 
 val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);