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.28  val Addsplits        = Splitter.Addsplits;
    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";