src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39650 2a35950ec495
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  declare le_bool_def_raw[code_pred_inline]
     1.5  
     1.6  lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
     1.7 -by (rule eq_reflection) (auto simp add: ext_iff min_def le_bool_def)
     1.8 +by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
     1.9  
    1.10  setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    1.11