src/HOL/Prod.ML
changeset 4830 bd73675adbed
parent 4828 ee3317896a47
child 4989 857dabe71d72
     1.1 --- a/src/HOL/Prod.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Prod.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -19,14 +19,14 @@
     1.4              rtac conjI, rtac refl, rtac refl]);
     1.5  qed "Pair_Rep_inject";
     1.6  
     1.7 -goal Prod.thy "inj_onto Abs_Prod Prod";
     1.8 -by (rtac inj_onto_inverseI 1);
     1.9 +goal Prod.thy "inj_on Abs_Prod Prod";
    1.10 +by (rtac inj_on_inverseI 1);
    1.11  by (etac Abs_Prod_inverse 1);
    1.12 -qed "inj_onto_Abs_Prod";
    1.13 +qed "inj_on_Abs_Prod";
    1.14  
    1.15  val prems = goalw Prod.thy [Pair_def]
    1.16      "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    1.17 -by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
    1.18 +by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
    1.19  by (REPEAT (ares_tac (prems@[ProdI]) 1));
    1.20  qed "Pair_inject";
    1.21  
    1.22 @@ -150,16 +150,16 @@
    1.23  by (stac surjective_pairing 1);
    1.24  by (stac split 1);
    1.25  by (Blast_tac 1);
    1.26 -qed "expand_split";
    1.27 +qed "split_split";
    1.28  
    1.29  (* could be done after split_tac has been speeded up significantly:
    1.30 -simpset_ref() := simpset() addsplits [expand_split];
    1.31 +simpset_ref() := simpset() addsplits [split_split];
    1.32     precompute the constants involved and don't do anything unless
    1.33     the current goal contains one of those constants
    1.34  *)
    1.35  
    1.36  goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
    1.37 -by (stac expand_split 1);
    1.38 +by (stac split_split 1);
    1.39  by (Simp_tac 1);
    1.40  qed "expand_split_asm";
    1.41