src/HOL/Inductive.thy
changeset 25510 38c15efe603b
parent 24915 fc90277c0dd7
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Inductive.thy	Fri Nov 30 16:23:52 2007 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Nov 30 20:13:03 2007 +0100
     1.3 @@ -290,8 +290,10 @@
     1.4  val def_gfp_unfold = @{thm def_gfp_unfold}
     1.5  val def_lfp_induct = @{thm def_lfp_induct}
     1.6  val def_coinduct = @{thm def_coinduct}
     1.7 -val inf_bool_eq = @{thm inf_bool_eq}
     1.8 -val inf_fun_eq = @{thm inf_fun_eq}
     1.9 +val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
    1.10 +val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
    1.11 +val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
    1.12 +val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
    1.13  val le_boolI = @{thm le_boolI}
    1.14  val le_boolI' = @{thm le_boolI'}
    1.15  val le_funI = @{thm le_funI}
    1.16 @@ -299,8 +301,8 @@
    1.17  val le_funE = @{thm le_funE}
    1.18  val le_boolD = @{thm le_boolD}
    1.19  val le_funD = @{thm le_funD}
    1.20 -val le_bool_def = @{thm le_bool_def}
    1.21 -val le_fun_def = @{thm le_fun_def}
    1.22 +val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
    1.23 +val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
    1.24  *}
    1.25  
    1.26  use "Tools/inductive_package.ML"