src/HOL/simpdata.ML
 changeset 7127 48e235179ffb parent 7031 972b5f62f476 child 7213 08a354bbc34c
```     1.1 --- a/src/HOL/simpdata.ML	Wed Jul 28 22:01:58 1999 +0200
1.2 +++ b/src/HOL/simpdata.ML	Thu Jul 29 12:44:57 1999 +0200
1.3 @@ -285,11 +285,11 @@
1.4  by (Blast_tac 1);
1.5  qed "if_False";
1.6
1.7 -Goalw [if_def] "!!P. P ==> (if P then x else y) = x";
1.8 +Goalw [if_def] "P ==> (if P then x else y) = x";
1.9  by (Blast_tac 1);
1.10  qed "if_P";
1.11
1.12 -Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y";
1.13 +Goalw [if_def] "~P ==> (if P then x else y) = y";
1.14  by (Blast_tac 1);
1.15  qed "if_not_P";
1.16
1.17 @@ -319,8 +319,7 @@
1.18  qed "if_eq_cancel";
1.19
1.20  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
1.21 -Goal
1.22 -    "(if P then Q else R) = ((P-->Q) & (~P-->R))";
1.23 +Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))";
1.24  by (rtac split_if 1);
1.25  qed "if_bool_eq_conj";
1.26
1.27 @@ -398,8 +397,6 @@
1.29  val Delsplits        = Splitter.Delsplits;
1.30
1.31 -(** 'if' congruence rules: neither included by default! *)
1.32 -
1.33  (*In general it seems wrong to add distributive laws by default: they
1.34    might cause exponential blow-up.  But imp_disjL has been in for a while
1.35    and cannot be removed without affecting existing proofs.  Moreover,
1.36 @@ -464,7 +461,8 @@
1.37  by (asm_simp_tac (HOL_ss addsimps prems) 1);
1.38  qed "if_cong";
1.39
1.40 -(*Prevents simplification of x and y: much faster*)
1.41 +(*Prevents simplification of x and y: faster and allows the execution
1.42 +  of functional programs. NOW THE DEFAULT.*)
1.43  Goal "b=c ==> (if b then x else y) = (if c then x else y)";
1.44  by (etac arg_cong 1);
1.45  qed "if_weak_cong";
```