| changeset 41075 | 4bed56dc95fb |
| parent 40548 | 54eb5fd36e5e |
| child 44241 | 7943b69f0188 |
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Dec 08 13:34:50 2010 +0100 @@ -7,7 +7,7 @@ declare HOL.if_bool_eq_disj[code_pred_inline] declare bool_diff_def[code_pred_inline] -declare inf_bool_eq_raw[code_pred_inline] +declare inf_bool_def_raw[code_pred_inline] declare less_bool_def_raw[code_pred_inline] declare le_bool_def_raw[code_pred_inline]