--- 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