src/HOL/Sum.ML
changeset 5316 7a8975451a89
parent 5183 89f162de39cf
child 7014 11ee650edcd2
     1.1 --- a/src/HOL/Sum.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -For Sum.thy.  The disjoint sum of two types
     1.8 +The disjoint sum of two types
     1.9  *)
    1.10  
    1.11  open Sum;
    1.12 @@ -51,13 +51,13 @@
    1.13  
    1.14  (** Injectiveness of Inl and Inr **)
    1.15  
    1.16 -val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
    1.17 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.18 +Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
    1.19 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.20  by (Blast_tac 1);
    1.21  qed "Inl_Rep_inject";
    1.22  
    1.23 -val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    1.24 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.25 +Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    1.26 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.27  by (Blast_tac 1);
    1.28  qed "Inr_Rep_inject";
    1.29  
    1.30 @@ -101,7 +101,7 @@
    1.31  
    1.32  (** Elimination rules **)
    1.33  
    1.34 -val major::prems = goalw Sum.thy [sum_def]
    1.35 +val major::prems = Goalw [sum_def]
    1.36      "[| u: A Plus B;  \
    1.37  \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
    1.38  \       !!y. [| y:B;  u=Inr(y) |] ==> P \
    1.39 @@ -130,7 +130,7 @@
    1.40  
    1.41  (** Exhaustion rule for sums -- a degenerate form of induction **)
    1.42  
    1.43 -val prems = goalw Sum.thy [Inl_def,Inr_def]
    1.44 +val prems = Goalw [Inl_def,Inr_def]
    1.45      "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
    1.46  \    |] ==> P";
    1.47  by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
    1.48 @@ -140,7 +140,7 @@
    1.49                      rtac (Rep_Sum_inverse RS sym)]));
    1.50  qed "sumE";
    1.51  
    1.52 -val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
    1.53 +val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
    1.54  by (res_inst_tac [("s","x")] sumE 1);
    1.55  by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
    1.56  qed "sum_induct";
    1.57 @@ -177,7 +177,7 @@
    1.58  
    1.59  val PartI = refl RSN (2,Part_eqI);
    1.60  
    1.61 -val major::prems = goalw Sum.thy [Part_def]
    1.62 +val major::prems = Goalw [Part_def]
    1.63      "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
    1.64  \    |] ==> P";
    1.65  by (rtac (major RS IntE) 1);