# HG changeset patch
# User wenzelm
# Date 1298043402 -3600
# Node ID 5f79a9e425075417e75928bc2f0880cb6fcdb045
# Parent  1f7cbe39d425d4ffd7a9d2f4d2d2556d6abb926c
modernized specifications;

diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/AxSem.thy
--- 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"
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Conform.thy
--- 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"
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Decl.thy
--- 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"
 
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/DeclConcepts.thy
--- 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 
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/DefiniteAssignment.thy
--- 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 *}
     
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Eval.thy
--- 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" 
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/State.thy
--- 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
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Table.thy
--- 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"
 
 
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Term.thy
--- 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"
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Value.thy
--- 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
diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/WellType.thy
--- 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"