src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 39302 d7728f65b353
parent 39200 bb93713b0925
child 39463 7ce0ed8dc4d6
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Mon Sep 13 11:13:15 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] ext_iff intro!: eq_reflection)
     1.8 +by (auto simp add: insert_iff[unfolded mem_def] fun_eq_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] ext_iff intro!: eq_reflection)
    1.12 +by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    1.13  
    1.14  setup {* Code_Prolog.map_code_options (K
    1.15    {ensure_groundness = true,