src/ZF/Inductive_ZF.thy
changeset 26480 544cef16045b
parent 26190 cf51a23c0cd0
child 29580 117b88da143c
     1.1 --- a/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  setup IndCases.setup
     1.5  setup DatatypeTactics.setup
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9  structure Lfp =
    1.10    struct
    1.11    val oper      = @{const lfp}