src/HOL/PreList.thy
changeset 14430 5cb24165a2e1
parent 14125 bf8edef6c1f1
child 14577 dbb95b825244
     1.1 --- a/src/HOL/PreList.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/PreList.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -9,7 +9,8 @@
     1.4  (*Is defined separately to serve as a basis for theory ToyList in the
     1.5  documentation.*)
     1.6  
     1.7 -theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
     1.8 +theory PreList =
     1.9 +    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
    1.10  
    1.11  (*belongs to theory Wellfounded_Recursion*)
    1.12  lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]