--- a/src/HOL/simpdata.ML Mon Mar 01 18:11:54 1999 +0100
+++ b/src/HOL/simpdata.ML Mon Mar 01 18:37:23 1999 +0100
@@ -356,24 +356,6 @@
(** 'if' congruence rules: neither included by default! *)
-(*Simplifies x assuming c and y assuming ~c*)
-qed_goal "if_cong" HOL.thy
- "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
-\ (if b then x else y) = (if c then u else v)"
- (fn rew::prems =>
- [stac rew 1, stac split_if 1, stac split_if 1,
- blast_tac (HOL_cs addDs prems) 1]);
-
-(*Prevents simplification of x and y: much faster*)
-qed_goal "if_weak_cong" HOL.thy
- "b=c ==> (if b then x else y) = (if c then x else y)"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
-
-(*Prevents simplification of t: much faster*)
-qed_goal "let_weak_cong" HOL.thy
- "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
-
(*In general it seems wrong to add distributive laws by default: they
might cause exponential blow-up. But imp_disjL has been in for a while
and cannot be removed without affecting existing proofs. Moreover,
@@ -431,6 +413,23 @@
addcongs [imp_cong]
addsplits [split_if];
+(*Simplifies x assuming c and y assuming ~c*)
+val prems = Goalw [if_def]
+ "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \
+\ (if b then x else y) = (if c then u else v)";
+by (asm_simp_tac (HOL_ss addsimps prems) 1);
+qed "if_cong";
+
+(*Prevents simplification of x and y: much faster*)
+qed_goal "if_weak_cong" HOL.thy
+ "b=c ==> (if b then x else y) = (if c then x else y)"
+ (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+(*Prevents simplification of t: much faster*)
+qed_goal "let_weak_cong" HOL.thy
+ "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
+ (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
qed_goal "if_distrib" HOL.thy
"f(if c then x else y) = (if c then f x else f y)"
(K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);