--- a/src/HOL/Induct/Acc.thy Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/Acc.thy Tue Jun 30 20:51:15 1998 +0200
@@ -9,7 +9,7 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-Acc = WF +
+Acc = WF + Inductive +
constdefs
pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)