src/ZF/ex/Acc.thy
changeset 809 1daa0269eb5d
parent 578 efc648d29dd0
child 1401 0c439768f45c
     1.1 --- a/src/ZF/ex/Acc.thy	Mon Dec 19 15:17:29 1994 +0100
     1.2 +++ b/src/ZF/ex/Acc.thy	Mon Dec 19 15:22:42 1994 +0100
     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 + "Inductive" +
     1.8 +Acc = WF + Inductive +
     1.9  
    1.10  consts
    1.11    acc :: "i=>i"