Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Bali/State.thy
changeset 14171 0cab06e3bbd0
parent 13688 a0b16d42d489
child 14766 c0401da7726d 
--- a/src/HOL/Bali/State.thy	Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/Bali/State.thy	Thu Aug 28 01:56:40 2003 +0200
@@ -266,7 +266,7 @@
 
 constdefs
   new_Addr     :: "heap \<Rightarrow> loc option"
- "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
+ "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
 
 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 apply (unfold new_Addr_def)
isabelle