| changeset 12667 | 7e6eaaa125f2 |
| parent 12620 | 4e6626725e21 |
| child 12776 | 249600a63ba9 |
--- a/src/ZF/Main.thy Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/Main.thy Tue Jan 08 16:09:09 2002 +0100 @@ -16,6 +16,7 @@ and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on] (* belongs to theory Ordinal *) +declare Ord_Least [intro,simp,TC] lemmas Ord_induct = Ord_induct [consumes 2] and Ord_induct_rule = Ord_induct [rule_format, consumes 2] and trans_induct = trans_induct [consumes 1]