--- a/src/HOL/Bali/AxSem.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy Fri Feb 18 16:36:42 2011 +0100
@@ -36,7 +36,7 @@
\end{itemize}
*}
-types res = vals --{* result entry *}
+type_synonym res = vals --{* result entry *}
abbreviation (input)
Val where "Val x == In1 x"
@@ -58,7 +58,7 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -381,7 +381,7 @@
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
-types 'a triples = "'a triple set"
+type_synonym 'a triples = "'a triple set"
abbreviation
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
--- a/src/HOL/Bali/Conform.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Conform.thy Fri Feb 18 16:36:42 2011 +0100
@@ -16,7 +16,7 @@
\end{itemize}
*}
-types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
section "extension of global store"
--- a/src/HOL/Bali/Decl.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Decl.thy Fri Feb 18 16:36:42 2011 +0100
@@ -136,7 +136,7 @@
subsubsection {* Static Modifier *}
-types stat_modi = bool (* modifier: static *)
+type_synonym stat_modi = bool (* modifier: static *)
subsection {* Declaration (base "class" for member,interface and class
declarations *}
@@ -164,8 +164,7 @@
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
-types
- fdecl (* field declaration, cf. 8.3 *)
+type_synonym fdecl (* field declaration, cf. 8.3 *)
= "vname \<times> field"
@@ -185,7 +184,7 @@
record methd = mhead + (* method in a class *)
mbody::mbody
-types mdecl = "sig \<times> methd" (* method declaration in a class *)
+type_synonym mdecl = "sig \<times> methd" (* method declaration in a class *)
translations
@@ -300,7 +299,7 @@
record iface = ibody + --{* interface *}
isuperIfs:: "qtname list" --{* superinterface list *}
-types
+type_synonym
idecl --{* interface declaration, cf. 9.1 *}
= "qtname \<times> iface"
@@ -332,7 +331,7 @@
record "class" = cbody + --{* class *}
super :: "qtname" --{* superclass *}
superIfs:: "qtname list" --{* implemented interfaces *}
-types
+type_synonym
cdecl --{* class declaration, cf. 8.1 *}
= "qtname \<times> class"
--- a/src/HOL/Bali/DeclConcepts.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Feb 18 16:36:42 2011 +0100
@@ -1401,7 +1401,7 @@
section "fields and methods"
-types
+type_synonym
fspec = "vname \<times> qtname"
translations
--- a/src/HOL/Bali/DefiniteAssignment.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Fri Feb 18 16:36:42 2011 +0100
@@ -498,7 +498,7 @@
section "The rules of definite assignment"
-types breakass = "(label, lname) tables"
+type_synonym breakass = "(label, lname) tables"
--{* Mapping from a break label, to the set of variables that will be assigned
if the evaluation terminates with this break *}
--- a/src/HOL/Bali/Eval.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Eval.thy Fri Feb 18 16:36:42 2011 +0100
@@ -96,8 +96,8 @@
*}
-types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- vals = "(val, vvar, val list) sum3"
+type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+type_synonym vals = "(val, vvar, val list) sum3"
translations
(type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
(type) "vals" <= (type) "(val, vvar, val list) sum3"
--- a/src/HOL/Bali/State.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/State.thy Fri Feb 18 16:36:42 2011 +0100
@@ -27,7 +27,7 @@
since its type is given already by the reference to
it (see below) *}
-types vn = "fspec + int" --{* variable name *}
+type_synonym vn = "fspec + int" --{* variable name *}
record obj =
tag :: "obj_tag" --{* generalized object *}
"values" :: "(vn, val) table"
@@ -130,7 +130,7 @@
section "object references"
-types oref = "loc + qtname" --{* generalized object reference *}
+type_synonym oref = "loc + qtname" --{* generalized object reference *}
syntax
Heap :: "loc \<Rightarrow> oref"
Stat :: "qtname \<Rightarrow> oref"
@@ -213,11 +213,11 @@
section "stores"
-types globs --{* global variables: heap and static variables *}
+type_synonym globs --{* global variables: heap and static variables *}
= "(oref , obj) table"
- heap
+type_synonym heap
= "(loc , obj) table"
-(* locals
+(* type_synonym locals
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
@@ -579,7 +579,7 @@
section "full program state"
-types
+type_synonym
state = "abopt \<times> st" --{* state including abruption information *}
translations
--- a/src/HOL/Bali/Table.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Table.thy Fri Feb 18 16:36:42 2011 +0100
@@ -29,9 +29,9 @@
\end{itemize}
*}
-types ('a, 'b) table --{* table with key type 'a and contents type 'b *}
+type_synonym ('a, 'b) table --{* table with key type 'a and contents type 'b *}
= "'a \<rightharpoonup> 'b"
- ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
+type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
= "'a \<Rightarrow> 'b set"
--- a/src/HOL/Bali/Term.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Term.thy Fri Feb 18 16:36:42 2011 +0100
@@ -57,7 +57,7 @@
-types locals = "(lname, val) table" --{* local variables *}
+type_synonym locals = "(lname, val) table" --{* local variables *}
datatype jump
@@ -78,7 +78,7 @@
| Jump jump --{* break, continue, return *}
| Error error -- {* runtime errors, we wan't to detect and proof absent
in welltyped programms *}
-types
+type_synonym
abopt = "abrupt option"
text {* Local variable store and exception.
@@ -235,7 +235,7 @@
intermediate steps of class-initialisation.
*}
-types "term" = "(expr+stmt,var,expr list) sum3"
+type_synonym "term" = "(expr+stmt,var,expr list) sum3"
translations
(type) "sig" <= (type) "mname \<times> ty list"
(type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
--- a/src/HOL/Bali/Value.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Value.thy Fri Feb 18 16:36:42 2011 +0100
@@ -26,7 +26,7 @@
primrec the_Addr :: "val \<Rightarrow> loc"
where "the_Addr (Addr a) = a"
-types dyn_ty = "loc \<Rightarrow> ty option"
+type_synonym dyn_ty = "loc \<Rightarrow> ty option"
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
where
--- a/src/HOL/Bali/WellType.thy Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/WellType.thy Fri Feb 18 16:36:42 2011 +0100
@@ -28,7 +28,7 @@
\end{itemize}
*}
-types lenv
+type_synonym lenv
= "(lname, ty) table" --{* local variables, including This and Result*}
record env =
@@ -49,7 +49,7 @@
section "Static overloading: maximally specific methods "
-types
+type_synonym
emhead = "ref_ty \<times> mhead"
--{* Some mnemotic selectors for emhead *}
@@ -244,7 +244,7 @@
section "Typing for terms"
-types tys = "ty + ty list"
+type_synonym tys = "ty + ty list"
translations
(type) "tys" <= (type) "ty + ty list"