src/ZF/Ordinal.thy

--- a/src/ZF/Ordinal.thy	Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/Ordinal.thy	Tue Aug 27 11:09:33 2002 +0200
@@ -328,11 +328,12 @@
 done
 
 (*Induction over an ordinal*)
-lemmas Ord_induct = Transset_induct [OF _ Ord_is_Transset]
+lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
+lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
 
 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
 
-lemma trans_induct:
+lemma trans_induct [consumes 1]:
     "[| Ord(i);  
         !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) |]
      ==>  P(i)"
@@ -340,6 +341,8 @@
 apply (blast intro: Ord_succ [THEN Ord_in_Ord]) 
 done
 
+lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
+
 
 (*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
 
@@ -684,7 +687,7 @@
      |] ==> P"
 by (drule Ord_cases_disj, blast)  
 
-lemma trans_induct3:
+lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
      "[| Ord(i);                 
          P(0);                   
          !!x. [| Ord(x);  P(x) |] ==> P(succ(x));        
@@ -694,6 +697,8 @@
 apply (erule Ord_cases, blast+)
 done
 
+lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
+
 text{*A set of ordinals is either empty, contains its own union, or its
 union is a limit ordinal.*}
 lemma Ord_set_cases:
@@ -721,14 +726,6 @@
 apply (blast intro!: equalityI)
 done
 
-(*special induction rules for the "induct" method*)
-lemmas Ord_induct = Ord_induct [consumes 2]
-  and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
-  and trans_induct = trans_induct [consumes 1]
-  and trans_induct_rule = trans_induct [rule_format, consumes 1]
-  and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
-  and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
-
 ML 
 {*
 val Memrel_def = thm "Memrel_def";