equal
deleted
inserted
replaced
14 |
14 |
15 definition |
15 definition |
16 less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)" |
16 less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)" |
17 |
17 |
18 instance |
18 instance |
19 by (intro_classes, auto simp add: less_bool_def) |
19 by (intro_classes, unfold less_bool_def, safe) |
20 |
20 |
21 end |
21 end |
22 |
22 |
23 lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)" |
23 lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)" |
24 by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq) |
24 by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq) |