# HG changeset patch
# User clasohm
# Date 817823870 -3600
# Node ID 007ad29ce6cacaaedbf7067fca549ca3ab2c8c84
# Parent  be42217b0b5c39f79d071a9f4f3ec95dede92e08
removed quotes from types section

diff -r be42217b0b5c -r 007ad29ce6ca src/HOL/Hoare/Hoare.thy
--- 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")
diff -r be42217b0b5c -r 007ad29ce6ca src/HOL/MiniML/Type.thy
--- 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
diff -r be42217b0b5c -r 007ad29ce6ca src/HOL/Univ.thy
--- 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)
diff -r be42217b0b5c -r 007ad29ce6ca src/HOL/ex/String.thy
--- 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 _")