src/HOL/Induct/Acc.thy
changeset 5102 8c782c25a11e
parent 3120 c58423c20740
child 5273 70f478d55606
     1.1 --- a/src/HOL/Induct/Acc.thy	Tue Jun 30 20:50:34 1998 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Tue Jun 30 20:51:15 1998 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     1.5  *)
     1.6  
     1.7 -Acc = WF + 
     1.8 +Acc = WF + Inductive +
     1.9  
    1.10  constdefs
    1.11    pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)