# HG changeset patch
# User wenzelm
# Date 1007828745 -3600
# Node ID 9032bdbc212506580dccf223f3b657c1ae67be15
# Parent  97975229f8933d59e4d876b658d021d498d49660
new-style theory;
proper declarations of various induction rules;

diff -r 97975229f893 -r 9032bdbc2125 src/ZF/Main.thy
--- a/src/ZF/Main.thy	Sat Dec 08 17:25:01 2001 +0100
+++ b/src/ZF/Main.thy	Sat Dec 08 17:25:45 2001 +0100
@@ -2,5 +2,49 @@
 (*$Id$
   theory Main includes everything*)
 
-Main = Update + InfDatatype + List + EquivClass + IntDiv
+theory Main = Update + InfDatatype + List + EquivClass + IntDiv:
+
+(* belongs to theory Trancl *)
+lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
+  and trancl_induct = trancl_induct [case_names initial step, induct set: trancl]
+  and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
+  and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
+
+(* belongs to theory WF *)
+lemmas wf_induct = wf_induct [induct set: wf]
+  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
+  and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
+  and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]
+
+(* belongs to theory Ordinal *)
+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]
 
+(* belongs to theory Nat *)
+lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
+  and complete_induct = complete_induct [case_names less, consumes 1]
+  and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1]
+  and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
+
+(* belongs to theory Epsilon *)
+lemmas eclose_induct = eclose_induct [induct set: eclose]
+  and eclose_induct_down = eclose_induct_down [consumes 1]
+
+(* belongs to theory Finite *)
+lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
+
+(* belongs to theory CardinalArith *)
+lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
+
+(* belongs to theory List *)
+lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
+
+(* belongs to theory IntDiv *)
+lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
+  and negDivAlg_induct = negDivAlg_induct [consumes 2]
+
+end