equal
deleted
inserted
replaced
7 declare Let_def[code_pred_inline] |
7 declare Let_def[code_pred_inline] |
8 |
8 |
9 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
9 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
10 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
10 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
11 |
11 |
12 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
12 lemma [code_pred_inline]: "(-) == (%A B x. A x \<and> \<not> B x)" |
13 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
13 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
14 |
14 |
15 instantiation room :: small_lazy |
15 instantiation room :: small_lazy |
16 begin |
16 begin |
17 |
17 |