src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 39200 bb93713b0925
parent 39189 d183bf90dabd
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 07 11:52:43 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 07 12:04:34 2010 +0200
     1.3 @@ -79,10 +79,10 @@
     1.4  declare Let_def[code_pred_inline]
     1.5  
     1.6  lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
     1.7 -by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     1.8 +by (auto simp add: insert_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
     1.9  
    1.10  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    1.11 -by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    1.12 +by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
    1.13  
    1.14  setup {* Code_Prolog.map_code_options (K
    1.15    {ensure_groundness = true,