author wenzelm Tue Feb 22 17:06:14 2011 +0100 (2011-02-22) changeset 41818 6d4c3ee8219d parent 41817 c7be23634728 child 41819 2d84831dc1a0
modernized specifications;
 src/HOL/Hahn_Banach/Function_Order.thy file | annotate | diff | revisions src/HOL/Induct/Com.thy file | annotate | diff | revisions src/HOL/Induct/Sexp.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Expr_Compiler.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare_Ex.thy file | annotate | diff | revisions
```     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.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
```