# HG changeset patch
# User wenzelm
# Date 1303556419 -7200
# Node ID f270e3e18be5187911d43a3e921289665e78e332
# Parent  0fd80c27fdf5bc5887ecd2999a0d11ef7ec1b4d9
modernized specifications;

diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -42,8 +42,8 @@
   but keeping them separate makes some later proofs simpler.
 *}
 
-types addr = nat -- "untyped heap references"
-types heap_rep = nat -- "representable values"
+type_synonym addr = nat -- "untyped heap references"
+type_synonym heap_rep = nat -- "representable values"
 
 record heap =
   arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -13,13 +13,13 @@
 subsection{* Types for Literals, Clauses and ProofSteps *}
 text {* We encode Literals as integers and Clauses as sorted Lists. *}
 
-types ClauseId = nat
-types Lit = int
-types Clause = "Lit list"
+type_synonym ClauseId = nat
+type_synonym Lit = int
+type_synonym Clause = "Lit list"
 
 text {* This resembles exactly to Isat's Proof Steps *}
 
-types Resolvants = "ClauseId * (Lit * ClauseId) list"
+type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
 datatype ProofStep =
   ProofDone bool
   | Root ClauseId Clause
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-types Num = "int \<times> int"
+type_synonym Num = "int \<times> int"
 
 abbreviation
   Num0_syn :: Num ("0\<^sub>N")
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -6,7 +6,7 @@
 imports Main "~~/src/HOL/Library/Lattice_Algebras"
 begin
 
-types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
+type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
 
 definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
   "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -6,9 +6,8 @@
 imports Matrix
 begin
 
-types 
-  'a spvec = "(nat * 'a) list"
-  'a spmat = "('a spvec) spvec"
+type_synonym 'a spvec = "(nat * 'a) list"
+type_synonym 'a spmat = "'a spvec spvec"
 
 definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix"
   where "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -14,8 +14,7 @@
 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
 by (metis Un_commute Un_left_absorb)
 
-types 
-  key = nat
+type_synonym key = nat
 
 consts
   all_symmetric :: bool        --{*true if all keys are symmetric*}
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,8 +9,7 @@
 imports JVMType "../JVM/JVMExceptions"
 begin
 
-types
-  succ_type = "(p_count \<times> state_type option) list"
+type_synonym succ_type = "(p_count \<times> state_type option) list"
 
 text {* Program counter of successor instructions: *}
 primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,14 +9,13 @@
 imports JType
 begin
 
-types
-  locvars_type = "ty err list"
-  opstack_type = "ty list"
-  state_type   = "opstack_type \<times> locvars_type"
-  state        = "state_type option err"    -- "for Kildall"
-  method_type  = "state_type option list"   -- "for BVSpec"
-  class_type   = "sig \<Rightarrow> method_type"
-  prog_type    = "cname \<Rightarrow> class_type"
+type_synonym locvars_type = "ty err list"
+type_synonym opstack_type = "ty list"
+type_synonym state_type = "opstack_type \<times> locvars_type"
+type_synonym state = "state_type option err"    -- "for Kildall"
+type_synonym method_type = "state_type option list"   -- "for BVSpec"
+type_synonym class_type = "sig \<Rightarrow> method_type"
+type_synonym prog_type = "cname \<Rightarrow> class_type"
 
 
 definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,7 +9,7 @@
 imports Typing_Framework_JVM
 begin
 
-types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
+type_synonym prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
 
 definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
   "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -11,8 +11,8 @@
 
 datatype 'a err = Err | OK 'a
 
-types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
-      'a esl =    "'a set * 'a ord * 'a ebinop"
+type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
+type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
 
 primrec ok_val :: "'a err \<Rightarrow> 'a" where
   "ok_val (OK x) = x"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,8 +9,7 @@
 imports SemilatAlg Opt
 begin
 
-types
-  's certificate = "'s list"   
+type_synonym 's certificate = "'s list"   
 
 primrec merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" where
   "merge cert f r T pc []     x = x"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -12,10 +12,9 @@
 imports Main "~~/src/HOL/Library/While_Combinator"
 begin
 
-types 
-  'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  'a sl     = "'a set \<times> 'a ord \<times> 'a binop"
+type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
 
 consts
   "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/DFA/Typing_Framework.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -12,8 +12,7 @@
 text {* 
   The relationship between dataflow analysis and a welltyped-instruction predicate. 
 *}
-types
-  's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
+type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
 
 definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -7,7 +7,7 @@
 
 theory Conform imports State WellType Exceptions begin
 
-types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
+type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
 
 definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
  "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -7,18 +7,23 @@
 
 theory Decl imports Type begin
 
-types 
+type_synonym 
   fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
 
+type_synonym
   sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
 
+type_synonym
   'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
 
+type_synonym
   'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
   -- "class = superclass, fields, methods"
 
+type_synonym
   'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
 
+type_synonym
   'c prog  = "'c cdecl list"     -- "program"
 
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,9 +9,10 @@
 imports TypeRel Value
 begin
 
-types 
+type_synonym 
   fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
 
+type_synonym
   obj = "cname \<times> fields'"    -- "class instance with class name and fields"
 
 definition obj_ty :: "obj => ty" where
@@ -20,11 +21,11 @@
 definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
 
-types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
-      locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
+type_synonym aheap = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
+type_synonym locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
 
-      state  = "aheap \<times> locals"      -- "heap, local parameter including This"
-      xstate = "val option \<times> state" -- "state including exception information"
+type_synonym state = "aheap \<times> locals"      -- "heap, local parameter including This"
+type_synonym xstate = "val option \<times> state" -- "state including exception information"
 
 abbreviation (input)
   heap :: "state => aheap"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -25,7 +25,7 @@
 \end{itemize}
 \end{description}
 *}
-types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
+type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
 
 definition wf_syscls :: "'c prog => bool" where
 "wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -22,9 +22,8 @@
 *}
 
 text "local variables, including method parameters and This:"
-types 
-  lenv   = "vname \<rightharpoonup> ty"
-  'c env = "'c prog \<times> lenv"
+type_synonym lenv = "vname \<rightharpoonup> ty"
+type_synonym 'c env = "'c prog \<times> lenv"
 
 abbreviation (input)
   prg :: "'c env => 'c prog"
@@ -99,7 +98,7 @@
 apply auto
 done
 
-types
+type_synonym
   java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
 -- "method body with parameter names, local variables, block, result expression."
 -- "local variables might include This, which is hidden anyway"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -28,13 +28,17 @@
         | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
         | Throw                     -- "throw top of stack as exception"
 
-types
+type_synonym
   bytecode = "instr list"
+type_synonym
   exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
                   -- "start-pc, end-pc, handler-pc, exception type"
+type_synonym
   exception_table = "exception_entry list"
+type_synonym
   jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
    -- "max stacksize, size of register set, instruction sequence, handler table"
+type_synonym
   jvm_prog = "jvm_method prog" 
 
 end
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -12,11 +12,11 @@
 begin
 
 section {* Frame Stack *}
-types
- opstack   = "val list"
- locvars   = "val list" 
- p_count   = nat
+type_synonym opstack = "val list"
+type_synonym locvars = "val list"
+type_synonym p_count = nat
 
+type_synonym
  frame = "opstack \<times>     
           locvars \<times>   
           cname \<times>     
@@ -35,7 +35,7 @@
   "raise_system_xcpt b x \<equiv> raise_if b x None"
 
 section {* Runtime State *}
-types
+type_synonym
   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -10,7 +10,7 @@
 imports HyperNat Real
 begin
 
-types hypreal = "real star"
+type_synonym hypreal = "real star"
 
 abbreviation
   hypreal_of_real :: "real => real star" where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/HyperNat.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -11,7 +11,7 @@
 imports StarDef
 begin
 
-types hypnat = "nat star"
+type_synonym hypnat = "nat star"
 
 abbreviation
   hypnat_of_nat :: "nat => nat star" where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,7 +9,7 @@
 imports Complex NSA
 begin
 
-types hcomplex = "complex star"
+type_synonym hcomplex = "complex star"
 
 abbreviation
   hcomplex_of_complex :: "complex => complex star" where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -6,10 +6,10 @@
 
 theory AxSem imports State begin
 
-types assn   = "state => bool"
-     vassn   = "val => assn"
-      triple = "assn \<times> stmt \<times>  assn"
-     etriple = "assn \<times> expr \<times> vassn"
+type_synonym assn = "state => bool"
+type_synonym vassn = "val => assn"
+type_synonym triple = "assn \<times> stmt \<times>  assn"
+type_synonym etriple = "assn \<times> expr \<times> vassn"
 translations
   (type) "assn" \<leftharpoondown> (type) "state => bool"
   (type) "vassn" \<leftharpoondown> (type) "val => assn"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NanoJava/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -12,7 +12,7 @@
   | Class cname  --{* class type *}
 
 text{* Field declaration *}
-types   fdecl           
+type_synonym fdecl           
         = "fname \<times> ty"
 
 record  methd           
@@ -22,7 +22,7 @@
           bdy :: stmt
 
 text{* Method declaration *}
-types   mdecl
+type_synonym mdecl
         = "mname \<times> methd"
 
 record  "class"
@@ -31,10 +31,10 @@
           methods ::"mdecl list"
 
 text{* Class declaration *}
-types   cdecl
+type_synonym cdecl
         = "cname \<times> class"
 
-types   prog
+type_synonym prog
         = "cdecl list"
 
 translations
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NanoJava/State.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -17,9 +17,10 @@
   = Null        --{* null reference *}
   | Addr loc    --{* address, i.e. location of object *}
 
-types   fields
+type_synonym fields
         = "(fname \<rightharpoonup> val)"
 
+type_synonym
         obj = "cname \<times> fields"
 
 translations
@@ -30,8 +31,8 @@
  "init_vars m == Option.map (\<lambda>T. Null) o m"
   
 text {* private: *}
-types   heap   = "loc   \<rightharpoonup> obj"
-        locals = "vname \<rightharpoonup> val"  
+type_synonym heap = "loc   \<rightharpoonup> obj"
+type_synonym locals = "vname \<rightharpoonup> val"  
 
 text {* private: *}
 record  state
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -19,7 +19,7 @@
 typedecl key
 typedecl room
 
-types keycard = "key \<times> key"
+type_synonym keycard = "key \<times> key"
 
 record state =
   owns :: "room \<Rightarrow> guest option"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -16,7 +16,7 @@
                             
 datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
 
-types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
+type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
 
 fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
 where
@@ -120,9 +120,8 @@
 
 subsection {* IMP *}
 
-types
-  var = nat
-  state = "int list"
+type_synonym var = nat
+type_synonym state = "int list"
 
 datatype com =
   Skip |
@@ -217,10 +216,9 @@
 
 text {* thanks to Elke Salecker *}
 
-types
-  vname = nat
-  vvalue = int
-  var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
+type_synonym vname = nat
+type_synonym vvalue = int
+type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
 
 datatype ir_expr = 
   IrConst vvalue
@@ -248,9 +246,8 @@
 
 subsection {* Another semantics *}
 
-types
-  name = nat --"For simplicity in examples"
-  state' = "name \<Rightarrow> nat"
+type_synonym name = nat --"For simplicity in examples"
+type_synonym state' = "name \<Rightarrow> nat"
 
 datatype aexp = N nat | V name | Plus aexp aexp
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -6,7 +6,7 @@
 datatype key = Key0 | Key1 | Key2 | Key3
 datatype room = Room0
 
-types card = "key * key"
+type_synonym card = "key * key"
 
 datatype event =
    Check_in guest room card | Enter guest room card | Exit guest room
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/IMP_4.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -8,9 +8,8 @@
   In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
 *}
 
-types
-  var = nat
-  state = "int list"
+type_synonym var = nat
+type_synonym state = "int list"
 
 datatype com =
   Skip |
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -176,9 +176,8 @@
 *)
 subsection {* IMP *}
 
-types
-  var = nat
-  state = "int list"
+type_synonym var = nat
+type_synonym state = "int list"
 
 datatype com =
   Skip |
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -770,9 +770,8 @@
 
 subsection {* IMP *}
 
-types
-  var = nat
-  state = "int list"
+type_synonym var = nat
+type_synonym state = "int list"
 
 datatype com =
   Skip |
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -110,7 +110,7 @@
   | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
 
 datatype binding = VarB type | TVarB type
-types env = "binding list"
+type_synonym env = "binding list"
 
 primrec is_TVarB :: "binding \<Rightarrow> bool"
 where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -32,8 +32,7 @@
 
 
 
-types
-  key = nat
+type_synonym key = nat
 
 consts
   all_symmetric :: bool        --{*true if all keys are symmetric*}
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -7,7 +7,7 @@
 
 theory Client imports "../Rename" AllocBase begin
 
-types
+type_synonym
   tokbag = nat     --{*tokbags could be multisets...or any ordered type?*}
 
 record state =
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/Counter.thy
--- a/src/HOL/UNITY/Comp/Counter.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -14,7 +14,7 @@
 
 (* Variables are names *)
 datatype name = C | c nat
-types state = "name=>int"
+type_synonym state = "name=>int"
 
 primrec sum  :: "[nat,state]=>int" where
   (* sum I s = sigma_{i<I}. s (c i) *)
@@ -25,7 +25,7 @@
   "sumj 0 i s = 0"
 | "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
   
-types command = "(state*state)set"
+type_synonym command = "(state*state)set"
 
 definition a :: "nat=>command" where
  "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -30,7 +30,7 @@
   "sumj 0 i s = 0"
 | "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
   
-types command = "(state*state)set"
+type_synonym command = "(state*state)set"
 
 definition a :: "nat=>command" where
  "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -12,8 +12,8 @@
    In J. Rolim (editor), Parallel and Distributed Processing,
    Spriner LNCS 1586 (1999), pages 1215-1227.*}
 
-types state = "(vertex*vertex)set"
-types command = "vertex=>(state*state)set"
+type_synonym state = "(vertex*vertex)set"
+type_synonym command = "vertex=>(state*state)set"
   
 consts
   init :: "(vertex*vertex)set"  
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -7,7 +7,7 @@
 
 theory TimerArray imports "../UNITY_Main" begin
 
-types 'a state = "nat * 'a"   (*second component allows new variables*)
+type_synonym 'a state = "nat * 'a"   (*second component allows new variables*)
 
 definition count :: "'a state => nat"
   where "count s = fst s"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/Channel.thy
--- a/src/HOL/UNITY/Simple/Channel.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/Channel.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,7 +9,7 @@
 
 theory Channel imports "../UNITY_Main" begin
 
-types state = "nat set"
+type_synonym state = "nat set"
 
 consts
   F :: "state program"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/Mutex.thy
--- a/src/HOL/UNITY/Simple/Mutex.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -14,7 +14,7 @@
   u :: bool
   v :: bool
 
-types command = "(state*state) set"
+type_synonym command = "(state*state) set"
 
 
   (** The program for process U **)
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -15,7 +15,7 @@
   Proc. Royal Soc. 426 (1989).
 *}
 
-types state = "event list"
+type_synonym state = "event list"
 
   (*The spy MAY say anything he CAN say.  We do not expect him to
     invent new nonces here, but he can also use NS1.  Common to
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/Network.thy
--- a/src/HOL/UNITY/Simple/Network.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -15,7 +15,7 @@
 
 datatype pname = Aproc | Bproc
 
-types state = "pname * pvar => nat"
+type_synonym state = "pname * pvar => nat"
 
 locale F_props =
   fixes F 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -10,7 +10,7 @@
 
 typedecl vertex
 
-types    state = "vertex=>bool"
+type_synonym state = "vertex=>bool"
 
 consts
   init ::  "vertex"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -10,7 +10,7 @@
 
 theory Reachability imports "../Detects" Reach begin
 
-types  edge = "(vertex*vertex)"
+type_synonym edge = "vertex * vertex"
 
 record state =
   reach :: "vertex => bool"
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -10,9 +10,9 @@
 imports Word
 begin
 
-types word32 = "32 word"
-types word8 = "8 word"
-types byte = word8
+type_synonym word32 = "32 word"
+type_synonym word8 = "8 word"
+type_synonym byte = word8
 
 -- "modulus"
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/CTL.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -21,7 +21,7 @@
 
 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
 
-types 'a ctl = "'a set"
+type_synonym 'a ctl = "'a set"
 
 definition
   imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -96,7 +96,7 @@
 
 subsection {* Colinearity is invariant by rotation *}
 
-types point = "int \<times> int"
+type_synonym point = "int \<times> int"
 
 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
   "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/RPred.thy
--- a/src/HOL/ex/RPred.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/RPred.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -2,7 +2,7 @@
 imports Quickcheck Random Predicate
 begin
 
-types 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+type_synonym 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
 
 section {* The RandomPred Monad *}
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/Records.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -235,7 +235,7 @@
 record 'a point'' = point +
   content :: 'a
 
-types cpoint'' = "colour point''"
+type_synonym cpoint'' = "colour point''"
 
 
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/Tree23.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -19,7 +19,7 @@
 function definitions take a few minutes and can also be seen as stress tests
 for the function definition facility.  *}
 
-types key = int -- {*for simplicity, should be a type class*}
+type_synonym key = int -- {*for simplicity, should be a type class*}
 
 datatype ord = LESS | EQUAL | GREATER
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/ex/Unification.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -31,8 +31,7 @@
   | Const 'a
   | App "'a trm" "'a trm" (infix "\<cdot>" 60)
 
-types
-  'a subst = "('a \<times> 'a trm) list"
+type_synonym 'a subst = "('a \<times> 'a trm) list"
 
 text {* Applying a substitution to a variable: *}
 
diff -r 0fd80c27fdf5 -r f270e3e18be5 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/Sequents/Sequents.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -40,17 +40,15 @@
  "_SeqO"           :: "o => seqobj"                        ("_")
  "_SeqId"          :: "'a => seqobj"                       ("$_")
 
-types
- single_seqe = "[seq,seqobj] => prop"
- single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
- two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
- two_seqe    = "[seq, seq] => prop"
- three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- three_seqe  = "[seq, seq, seq] => prop"
- four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- four_seqe   = "[seq, seq, seq, seq] => prop"
-
- sequence_name = "seq'=>seq'"
+type_synonym single_seqe = "[seq,seqobj] => prop"
+type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
+type_synonym two_seqe = "[seq, seq] => prop"
+type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+type_synonym three_seqe = "[seq, seq, seq] => prop"
+type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
+type_synonym sequence_name = "seq'=>seq'"
 
 
 syntax