modernized specifications;
authorwenzelm
Tue Feb 22 17:06:14 2011 +0100 (2011-02-22)
changeset 418186d4c3ee8219d
parent 41817 c7be23634728
child 41819 2d84831dc1a0
modernized specifications;
src/HOL/Hahn_Banach/Function_Order.thy
src/HOL/Induct/Com.thy
src/HOL/Induct/Sexp.thy
src/HOL/Isar_Examples/Expr_Compiler.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Isar_Examples/Hoare_Ex.thy
     1.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 16:47:18 2011 +0100
     1.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 17:06:14 2011 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    graph.
     1.5  *}
     1.6  
     1.7 -types 'a graph = "('a \<times> real) set"
     1.8 +type_synonym 'a graph = "('a \<times> real) set"
     1.9  
    1.10  definition
    1.11    graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
     2.1 --- a/src/HOL/Induct/Com.thy	Tue Feb 22 16:47:18 2011 +0100
     2.2 +++ b/src/HOL/Induct/Com.thy	Tue Feb 22 17:06:14 2011 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  theory Com imports Main begin
     2.5  
     2.6  typedecl loc
     2.7 -types  state = "loc => nat"
     2.8 +type_synonym state = "loc => nat"
     2.9  
    2.10  datatype
    2.11    exp = N nat
     3.1 --- a/src/HOL/Induct/Sexp.thy	Tue Feb 22 16:47:18 2011 +0100
     3.2 +++ b/src/HOL/Induct/Sexp.thy	Tue Feb 22 17:06:14 2011 +0100
     3.3 @@ -8,8 +8,7 @@
     3.4  
     3.5  theory Sexp imports Main begin
     3.6  
     3.7 -types
     3.8 -  'a item = "'a Datatype.item"
     3.9 +type_synonym 'a item = "'a Datatype.item"
    3.10  abbreviation "Leaf == Datatype.Leaf"
    3.11  abbreviation "Numb == Datatype.Numb"
    3.12  
     4.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 22 16:47:18 2011 +0100
     4.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 22 17:06:14 2011 +0100
     4.3 @@ -22,8 +22,7 @@
     4.4    This is both for abstract syntax and semantics, i.e.\ we use a
     4.5    ``shallow embedding'' here. *}
     4.6  
     4.7 -types
     4.8 -  'val binop = "'val => 'val => 'val"
     4.9 +type_synonym 'val binop = "'val => 'val => 'val"
    4.10  
    4.11  
    4.12  subsection {* Expressions *}
     5.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 16:47:18 2011 +0100
     5.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 17:06:14 2011 +0100
     5.3 @@ -19,9 +19,8 @@
     5.4    \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
     5.5    \cite{Nipkow:1998:Winskel}. *}
     5.6  
     5.7 -types
     5.8 -  'a bexp = "'a set"
     5.9 -  'a assn = "'a set"
    5.10 +type_synonym 'a bexp = "'a set"
    5.11 +type_synonym 'a assn = "'a set"
    5.12  
    5.13  datatype 'a com =
    5.14      Basic "'a => 'a"
    5.15 @@ -32,8 +31,7 @@
    5.16  abbreviation Skip  ("SKIP")
    5.17    where "SKIP == Basic id"
    5.18  
    5.19 -types
    5.20 -  'a sem = "'a => 'a => bool"
    5.21 +type_synonym 'a sem = "'a => 'a => bool"
    5.22  
    5.23  primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
    5.24  where
     6.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 22 16:47:18 2011 +0100
     6.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 22 17:06:14 2011 +0100
     6.3 @@ -256,7 +256,7 @@
     6.4  
     6.5  record tstate = time :: nat
     6.6  
     6.7 -types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
     6.8 +type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
     6.9  
    6.10  primrec timeit :: "'a time com \<Rightarrow> 'a time com"
    6.11  where