--- a/src/HOL/Hoare/Hoare.thy Fri Dec 01 13:54:27 1995 +0100
+++ b/src/HOL/Hoare/Hoare.thy Fri Dec 01 14:17:50 1995 +0100
@@ -10,11 +10,11 @@
types
'a prog (* program syntax *)
- pvar = "nat" (* encoding of program variables ( < 26! ) *)
- 'a state = "pvar => 'a" (* program state *)
- 'a exp ="'a state => 'a" (* denotation of expressions *)
- 'a bexp = "'a state => bool" (* denotation of boolean expressions *)
- 'a com = "'a state => 'a state => bool" (* denotation of programs *)
+ pvar = nat (* encoding of program variables ( < 26! ) *)
+ 'a state = pvar => 'a (* program state *)
+ 'a exp = 'a state => 'a (* denotation of expressions *)
+ 'a bexp = 'a state => bool (* denotation of boolean expressions *)
+ 'a com = 'a state => 'a state => bool (* denotation of programs *)
syntax
"@Skip" :: 'a prog ("SKIP")