src/HOL/Hoare/Pointer_Examples.thy

--- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:22:14 2010 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 18:41:06 2010 +0200
@@ -216,18 +216,19 @@
 
 text"This is still a bit rough, especially the proof."
 
-definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cor P Q == if P then True else Q"
+definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cor P Q \<longleftrightarrow> (if P then True else Q)"
 
-definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cand P Q == if P then Q else False"
+definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cand P Q \<longleftrightarrow> (if P then Q else False)"
 
-fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
-"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
-                                else y # merge(x#xs,ys,f))" |
-"merge(x#xs,[],f) = x # merge(xs,[],f)" |
-"merge([],y#ys,f) = y # merge([],ys,f)" |
-"merge([],[],f) = []"
+fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
+where
+  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
+                                  else y # merge(x#xs,ys,f))"
+| "merge(x#xs,[],f) = x # merge(xs,[],f)"
+| "merge([],y#ys,f) = y # merge([],ys,f)"
+| "merge([],[],f) = []"
 
 text{* Simplifies the proof a little: *}
 
@@ -336,8 +337,9 @@
 Path}. Since the result is not that convincing, we do not prove any of
 the lemmas.*}
 
-consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
-       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+axiomatization
+  ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
+  path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
 
 text"First some basic lemmas:"
 
@@ -479,8 +481,8 @@
 
 subsection "Storage allocation"
 
-definition new :: "'a set \<Rightarrow> 'a" where
-"new A == SOME a. a \<notin> A"
+definition new :: "'a set \<Rightarrow> 'a"
+  where "new A = (SOME a. a \<notin> A)"
 
 
 lemma new_notin: