# HG changeset patch
# User wenzelm
# Date 897392983 -7200
# Node ID 0ebd6c91088a1b9546313a3836496fe25d4b5e2b
# Parent  cdc86a914e633dfe5bc9bcf64dc3614fe5750c96
nonterminals prog;

diff -r cdc86a914e63 -r 0ebd6c91088a src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Tue Jun 09 11:37:52 1998 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Tue Jun 09 13:49:43 1998 +0200
@@ -9,27 +9,30 @@
 Hoare = Arith +
 
 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 *)
+
+
+(* program syntax *)
+
+nonterminals
+  prog
 
 syntax
-  "@Skip"       :: 'a prog                              ("SKIP")
-  "@Assign"     :: [id, 'a] => 'a prog          ("_ := _")
-  "@Seq"        :: ['a prog, 'a prog] => 'a prog        ("_;//_" [0,1000] 999)
-  "@If"         :: [bool, 'a prog, 'a prog] => 'a prog
-                   ("IF _//THEN//  (_)//ELSE//  (_)//END")
-  "@While"      :: [bool, bool, 'a prog] => 'a prog
-                   ("WHILE _//DO {_}//  (_)//END")
+  "@Skip"       :: prog                         ("SKIP")
+  "@Assign"     :: [id, 'a] => prog             ("_ := _")
+  "@Seq"        :: [prog, prog] => prog         ("_;//_" [0,1000] 999)
+  "@If"         :: [bool, prog, prog] => prog   ("IF _//THEN//  (_)//ELSE//  (_)//END")
+  "@While"      :: [bool, bool, prog] => prog   ("WHILE _//DO {_}//  (_)//END")
+  "@Spec"       :: [bool, prog, bool] => bool   ("{_}//_//{_}")
 
-  "@Spec"       :: [bool, 'a prog, bool] => bool        ("{_}//_//{_}")
+
+(* denotational semantics *)
 
 constdefs
-  (* denotational semantics *)
-
   Skip          :: 'a com
   "Skip s s' == (s=s')"