src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 39302 d7728f65b353
parent 39250 548a3e5521ab
child 40173 0ffdd6baec03
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  lemma Heap_eqI:
     1.6    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
     1.7 -    by (cases f, cases g) (auto simp: ext_iff)
     1.8 +    by (cases f, cases g) (auto simp: fun_eq_iff)
     1.9  
    1.10  ML {* structure Execute_Simps = Named_Thms(
    1.11    val name = "execute_simps"