src/HOL/Inductive.thy
changeset 32652 3175e23b79f3
parent 32587 caa5ada96a00
child 32701 5059a733a4b8
     1.1 --- a/src/HOL/Inductive.thy	Wed Sep 23 11:33:52 2009 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Sep 23 12:03:47 2009 +0200
     1.3 @@ -267,26 +267,6 @@
     1.4    Ball_def Bex_def
     1.5    induct_rulify_fallback
     1.6  
     1.7 -ML {*
     1.8 -val def_lfp_unfold = @{thm def_lfp_unfold}
     1.9 -val def_gfp_unfold = @{thm def_gfp_unfold}
    1.10 -val def_lfp_induct = @{thm def_lfp_induct}
    1.11 -val def_coinduct = @{thm def_coinduct}
    1.12 -val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
    1.13 -val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
    1.14 -val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
    1.15 -val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
    1.16 -val le_boolI = @{thm le_boolI}
    1.17 -val le_boolI' = @{thm le_boolI'}
    1.18 -val le_funI = @{thm le_funI}
    1.19 -val le_boolE = @{thm le_boolE}
    1.20 -val le_funE = @{thm le_funE}
    1.21 -val le_boolD = @{thm le_boolD}
    1.22 -val le_funD = @{thm le_funD}
    1.23 -val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
    1.24 -val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
    1.25 -*}
    1.26 -
    1.27  use "Tools/inductive.ML"
    1.28  setup Inductive.setup
    1.29