--- 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")
--- a/src/HOL/MiniML/Type.thy Fri Dec 01 13:54:27 1995 +0100
+++ b/src/HOL/MiniML/Type.thy Fri Dec 01 14:17:50 1995 +0100
@@ -18,7 +18,7 @@
(* type variable substitution *)
types
- subst = "nat => type_expr"
+ subst = nat => type_expr
arities
type_expr::type_struct
--- a/src/HOL/Univ.thy Fri Dec 01 13:54:27 1995 +0100
+++ b/src/HOL/Univ.thy Fri Dec 01 14:17:50 1995 +0100
@@ -19,7 +19,7 @@
'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
types
- 'a item = "'a node set"
+ 'a item = 'a node set
consts
Least :: (nat=>bool) => nat (binder "LEAST " 10)
--- a/src/HOL/ex/String.thy Fri Dec 01 13:54:27 1995 +0100
+++ b/src/HOL/ex/String.thy Fri Dec 01 14:17:50 1995 +0100
@@ -14,7 +14,7 @@
char = Char nibble nibble
types
- string = "char list"
+ string = char list
syntax
"_Char" :: xstr => char ("CHR _")