modernized specifications;

--- a/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -21,7 +21,7 @@
   graph.
 *}
 
-types 'a graph = "('a \<times> real) set"
+type_synonym 'a graph = "('a \<times> real) set"
 
 definition
   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where

--- a/src/HOL/Induct/Com.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Induct/Com.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -10,7 +10,7 @@
 theory Com imports Main begin
 
 typedecl loc
-types  state = "loc => nat"
+type_synonym state = "loc => nat"
 
 datatype
   exp = N nat

--- a/src/HOL/Induct/Sexp.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Induct/Sexp.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -8,8 +8,7 @@
 
 theory Sexp imports Main begin
 
-types
-  'a item = "'a Datatype.item"
+type_synonym 'a item = "'a Datatype.item"
 abbreviation "Leaf == Datatype.Leaf"
 abbreviation "Numb == Datatype.Numb"
 

--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -22,8 +22,7 @@
   This is both for abstract syntax and semantics, i.e.\ we use a
   ``shallow embedding'' here. *}
 
-types
-  'val binop = "'val => 'val => 'val"
+type_synonym 'val binop = "'val => 'val => 'val"
 
 
 subsection {* Expressions *}

--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -19,9 +19,8 @@
   \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
   \cite{Nipkow:1998:Winskel}. *}
 
-types
-  'a bexp = "'a set"
-  'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 datatype 'a com =
     Basic "'a => 'a"
@@ -32,8 +31,7 @@
 abbreviation Skip  ("SKIP")
   where "SKIP == Basic id"
 
-types
-  'a sem = "'a => 'a => bool"
+type_synonym 'a sem = "'a => 'a => bool"
 
 primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
 where

--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -256,7 +256,7 @@
 
 record tstate = time :: nat
 
-types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
+type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
 
 primrec timeit :: "'a time com \<Rightarrow> 'a time com"
 where