added split_all_tac to claset()
authoroheimb
Wed Feb 25 15:48:04 1998 +0100 (1998-02-25)
changeset 465091af1ef45d68
parent 4649 89ad3eb863a1
child 4651 70dd492a1698
added split_all_tac to claset()
src/HOL/Prod.ML
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Prod.ML	Wed Feb 25 15:45:32 1998 +0100
     1.2 +++ b/src/HOL/Prod.ML	Wed Feb 25 15:48:04 1998 +0100
     1.3 @@ -80,9 +80,8 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -(* Could be nice, but breaks too many proofs:
     1.8 -claset_ref() := claset() addbefore split_all_tac;
     1.9 -*)
    1.10 +(* consider addSbefore ?? *)
    1.11 +claset_ref() := claset() addbefore ("split_all_tac",split_all_tac);
    1.12  
    1.13  (*** lemmas for splitting paired `!!'
    1.14  Does not work with simplifier because it also affects premises in
    1.15 @@ -120,13 +119,13 @@
    1.16  ***)
    1.17  
    1.18  goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
    1.19 -by (fast_tac (claset() addbefore split_all_tac) 1);
    1.20 +by (Fast_tac 1);
    1.21  qed "split_paired_All";
    1.22  Addsimps [split_paired_All];
    1.23  (* AddIffs is not a good idea because it makes Blast_tac loop *)
    1.24  
    1.25  goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
    1.26 -by (fast_tac (claset() addbefore split_all_tac) 1);
    1.27 +by (Fast_tac 1);
    1.28  qed "split_paired_Ex";
    1.29  Addsimps [split_paired_Ex];
    1.30  
     2.1 --- a/src/HOL/Relation.ML	Wed Feb 25 15:45:32 1998 +0100
     2.2 +++ b/src/HOL/Relation.ML	Wed Feb 25 15:48:04 1998 +0100
     2.3 @@ -215,11 +215,11 @@
     2.4      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
     2.5  
     2.6  goal Relation.thy "R O id = R";
     2.7 -by (fast_tac (claset() addbefore split_all_tac) 1);
     2.8 +by (Fast_tac 1);
     2.9  qed "R_O_id";
    2.10  
    2.11  goal Relation.thy "id O R = R";
    2.12 -by (fast_tac (claset() addbefore split_all_tac) 1);
    2.13 +by (Fast_tac 1);
    2.14  qed "id_O_R";
    2.15  
    2.16  Addsimps [R_O_id,id_O_R];