equal
deleted
inserted
replaced
77 lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) |
77 lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) |
78 |
78 |
79 declare Let_def[code_pred_inline] |
79 declare Let_def[code_pred_inline] |
80 |
80 |
81 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
81 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
82 by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) |
82 by (auto simp add: insert_iff[unfolded mem_def] ext_iff intro!: eq_reflection) |
83 |
83 |
84 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
84 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
85 by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) |
85 by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection) |
86 |
86 |
87 setup {* Code_Prolog.map_code_options (K |
87 setup {* Code_Prolog.map_code_options (K |
88 {ensure_groundness = true, |
88 {ensure_groundness = true, |
89 limited_types = [], |
89 limited_types = [], |
90 limited_predicates = [], |
90 limited_predicates = [], |