src/HOL/Hoare/Pointer_Examples.thy
changeset 35416 d8d7d1b785af
parent 35316 870dfea4f9c0
child 35419 d78659d1723e
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -216,10 +216,10 @@
     1.4  
     1.5  text"This is still a bit rough, especially the proof."
     1.6  
     1.7 -constdefs
     1.8 - cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     1.9 +definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.10  "cor P Q == if P then True else Q"
    1.11 - cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    1.12 +
    1.13 +definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.14  "cand P Q == if P then Q else False"
    1.15  
    1.16  consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
    1.17 @@ -481,7 +481,7 @@
    1.18  
    1.19  subsection "Storage allocation"
    1.20  
    1.21 -constdefs new :: "'a set \<Rightarrow> 'a"
    1.22 +definition new :: "'a set \<Rightarrow> 'a" where
    1.23  "new A == SOME a. a \<notin> A"
    1.24  
    1.25