equal
deleted
inserted
replaced
5 section {* Common constants *} |
5 section {* Common constants *} |
6 |
6 |
7 declare HOL.if_bool_eq_disj[code_pred_inline] |
7 declare HOL.if_bool_eq_disj[code_pred_inline] |
8 |
8 |
9 declare bool_diff_def[code_pred_inline] |
9 declare bool_diff_def[code_pred_inline] |
10 declare inf_bool_eq_raw[code_pred_inline] |
10 declare inf_bool_def_raw[code_pred_inline] |
11 declare less_bool_def_raw[code_pred_inline] |
11 declare less_bool_def_raw[code_pred_inline] |
12 declare le_bool_def_raw[code_pred_inline] |
12 declare le_bool_def_raw[code_pred_inline] |
13 |
13 |
14 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)" |
14 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)" |
15 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def) |
15 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def) |