tidied; added lemma restrict_to_left
authorpaulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23 ago)
changeset 75845be4bb8e4e3f
parent 7583 d1b40e0464b1
child 7585 dca904d4ce4c
tidied; added lemma restrict_to_left
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 23 09:05:44 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 23 13:06:31 1999 +0200
     1.3 @@ -480,12 +480,11 @@
     1.4  by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
     1.5  qed "if_distrib";
     1.6  
     1.7 -
     1.8  (*For expand_case_tac*)
     1.9 -val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
    1.10 +val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
    1.11  by (case_tac "P" 1);
    1.12  by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
    1.13 -val expand_case = result();
    1.14 +qed "expand_case";
    1.15  
    1.16  (*Used in Auth proofs.  Typically P contains Vars that become instantiated
    1.17    during unification.*)
    1.18 @@ -494,9 +493,16 @@
    1.19      Simp_tac (i+1) THEN 
    1.20      Simp_tac i;
    1.21  
    1.22 +(*This lemma restricts the effect of the rewrite rule u=v to the left-hand
    1.23 +  side of an equality.  Used in {Integ,Real}/simproc.ML*)
    1.24 +Goal "x=y ==> (x=z) = (y=z)";
    1.25 +by (asm_simp_tac HOL_ss 1);
    1.26 +qed "restrict_to_left";
    1.27  
    1.28  (* default simpset *)
    1.29 -val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
    1.30 +val simpsetup = 
    1.31 +    [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; 
    1.32 +		thy)];
    1.33  
    1.34  
    1.35  (*** integration of simplifier with classical reasoner ***)