--- a/src/HOL/PreList.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/PreList.thy Thu Mar 04 12:06:07 2004 +0100
@@ -9,7 +9,8 @@
(*Is defined separately to serve as a basis for theory ToyList in the
documentation.*)
-theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
+theory PreList =
+ Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
(*belongs to theory Wellfounded_Recursion*)
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]