modernized specifications;
authorwenzelm
Sat Apr 23 13:00:19 2011 +0200 (2011-04-23)
changeset 42463f270e3e18be5
parent 42462 0fd80c27fdf5
child 42464 ae16b8abf1a8
modernized specifications;
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/DFA/LBVSpec.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/DFA/Typing_Framework.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/JVMInstructions.thy
src/HOL/MicroJava/JVM/JVMState.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/HyperNat.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/State.thy
src/HOL/Nitpick_Examples/Hotel_Nits.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/IMP_4.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/UNITY/Comp/Client.thy
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Comp/TimerArray.thy
src/HOL/UNITY/Simple/Channel.thy
src/HOL/UNITY/Simple/Mutex.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/Simple/Network.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/Word/Examples/WordExamples.thy
src/HOL/ex/CTL.thy
src/HOL/ex/Groebner_Examples.thy
src/HOL/ex/RPred.thy
src/HOL/ex/Records.thy
src/HOL/ex/Tree23.thy
src/HOL/ex/Unification.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4    but keeping them separate makes some later proofs simpler.
     1.5  *}
     1.6  
     1.7 -types addr = nat -- "untyped heap references"
     1.8 -types heap_rep = nat -- "representable values"
     1.9 +type_synonym addr = nat -- "untyped heap references"
    1.10 +type_synonym heap_rep = nat -- "representable values"
    1.11  
    1.12  record heap =
    1.13    arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
     2.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Apr 22 15:57:43 2011 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sat Apr 23 13:00:19 2011 +0200
     2.3 @@ -13,13 +13,13 @@
     2.4  subsection{* Types for Literals, Clauses and ProofSteps *}
     2.5  text {* We encode Literals as integers and Clauses as sorted Lists. *}
     2.6  
     2.7 -types ClauseId = nat
     2.8 -types Lit = int
     2.9 -types Clause = "Lit list"
    2.10 +type_synonym ClauseId = nat
    2.11 +type_synonym Lit = int
    2.12 +type_synonym Clause = "Lit list"
    2.13  
    2.14  text {* This resembles exactly to Isat's Proof Steps *}
    2.15  
    2.16 -types Resolvants = "ClauseId * (Lit * ClauseId) list"
    2.17 +type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
    2.18  datatype ProofStep =
    2.19    ProofDone bool
    2.20    | Root ClauseId Clause
     3.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Apr 22 15:57:43 2011 +0200
     3.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Apr 23 13:00:19 2011 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  imports Complex_Main
     3.5  begin
     3.6  
     3.7 -types Num = "int \<times> int"
     3.8 +type_synonym Num = "int \<times> int"
     3.9  
    3.10  abbreviation
    3.11    Num0_syn :: Num ("0\<^sub>N")
     4.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Apr 22 15:57:43 2011 +0200
     4.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Apr 23 13:00:19 2011 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  imports Main "~~/src/HOL/Library/Lattice_Algebras"
     4.5  begin
     4.6  
     4.7 -types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
     4.8 +type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
     4.9  
    4.10  definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
    4.11    "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
     5.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Apr 22 15:57:43 2011 +0200
     5.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Sat Apr 23 13:00:19 2011 +0200
     5.3 @@ -6,9 +6,8 @@
     5.4  imports Matrix
     5.5  begin
     5.6  
     5.7 -types 
     5.8 -  'a spvec = "(nat * 'a) list"
     5.9 -  'a spmat = "('a spvec) spvec"
    5.10 +type_synonym 'a spvec = "(nat * 'a) list"
    5.11 +type_synonym 'a spmat = "'a spvec spvec"
    5.12  
    5.13  definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix"
    5.14    where "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
     6.1 --- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 22 15:57:43 2011 +0200
     6.2 +++ b/src/HOL/Metis_Examples/Message.thy	Sat Apr 23 13:00:19 2011 +0200
     6.3 @@ -14,8 +14,7 @@
     6.4  lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
     6.5  by (metis Un_commute Un_left_absorb)
     6.6  
     6.7 -types 
     6.8 -  key = nat
     6.9 +type_synonym key = nat
    6.10  
    6.11  consts
    6.12    all_symmetric :: bool        --{*true if all keys are symmetric*}
     7.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Fri Apr 22 15:57:43 2011 +0200
     7.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Sat Apr 23 13:00:19 2011 +0200
     7.3 @@ -9,8 +9,7 @@
     7.4  imports JVMType "../JVM/JVMExceptions"
     7.5  begin
     7.6  
     7.7 -types
     7.8 -  succ_type = "(p_count \<times> state_type option) list"
     7.9 +type_synonym succ_type = "(p_count \<times> state_type option) list"
    7.10  
    7.11  text {* Program counter of successor instructions: *}
    7.12  primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where
     8.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Fri Apr 22 15:57:43 2011 +0200
     8.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sat Apr 23 13:00:19 2011 +0200
     8.3 @@ -9,14 +9,13 @@
     8.4  imports JType
     8.5  begin
     8.6  
     8.7 -types
     8.8 -  locvars_type = "ty err list"
     8.9 -  opstack_type = "ty list"
    8.10 -  state_type   = "opstack_type \<times> locvars_type"
    8.11 -  state        = "state_type option err"    -- "for Kildall"
    8.12 -  method_type  = "state_type option list"   -- "for BVSpec"
    8.13 -  class_type   = "sig \<Rightarrow> method_type"
    8.14 -  prog_type    = "cname \<Rightarrow> class_type"
    8.15 +type_synonym locvars_type = "ty err list"
    8.16 +type_synonym opstack_type = "ty list"
    8.17 +type_synonym state_type = "opstack_type \<times> locvars_type"
    8.18 +type_synonym state = "state_type option err"    -- "for Kildall"
    8.19 +type_synonym method_type = "state_type option list"   -- "for BVSpec"
    8.20 +type_synonym class_type = "sig \<Rightarrow> method_type"
    8.21 +type_synonym prog_type = "cname \<Rightarrow> class_type"
    8.22  
    8.23  
    8.24  definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where
     9.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Fri Apr 22 15:57:43 2011 +0200
     9.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Sat Apr 23 13:00:19 2011 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4  imports Typing_Framework_JVM
     9.5  begin
     9.6  
     9.7 -types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
     9.8 +type_synonym prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
     9.9  
    9.10  definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
    9.11    "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
    10.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Fri Apr 22 15:57:43 2011 +0200
    10.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Sat Apr 23 13:00:19 2011 +0200
    10.3 @@ -11,8 +11,8 @@
    10.4  
    10.5  datatype 'a err = Err | OK 'a
    10.6  
    10.7 -types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
    10.8 -      'a esl =    "'a set * 'a ord * 'a ebinop"
    10.9 +type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
   10.10 +type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
   10.11  
   10.12  primrec ok_val :: "'a err \<Rightarrow> 'a" where
   10.13    "ok_val (OK x) = x"
    11.1 --- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Fri Apr 22 15:57:43 2011 +0200
    11.2 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Sat Apr 23 13:00:19 2011 +0200
    11.3 @@ -9,8 +9,7 @@
    11.4  imports SemilatAlg Opt
    11.5  begin
    11.6  
    11.7 -types
    11.8 -  's certificate = "'s list"   
    11.9 +type_synonym 's certificate = "'s list"   
   11.10  
   11.11  primrec merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" where
   11.12    "merge cert f r T pc []     x = x"
    12.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Fri Apr 22 15:57:43 2011 +0200
    12.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sat Apr 23 13:00:19 2011 +0200
    12.3 @@ -12,10 +12,9 @@
    12.4  imports Main "~~/src/HOL/Library/While_Combinator"
    12.5  begin
    12.6  
    12.7 -types 
    12.8 -  'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    12.9 -  'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   12.10 -  'a sl     = "'a set \<times> 'a ord \<times> 'a binop"
   12.11 +type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
   12.12 +type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   12.13 +type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
   12.14  
   12.15  consts
   12.16    "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    13.1 --- a/src/HOL/MicroJava/DFA/Typing_Framework.thy	Fri Apr 22 15:57:43 2011 +0200
    13.2 +++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy	Sat Apr 23 13:00:19 2011 +0200
    13.3 @@ -12,8 +12,7 @@
    13.4  text {* 
    13.5    The relationship between dataflow analysis and a welltyped-instruction predicate. 
    13.6  *}
    13.7 -types
    13.8 -  's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
    13.9 +type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
   13.10  
   13.11  definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
   13.12  "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
    14.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Apr 22 15:57:43 2011 +0200
    14.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Sat Apr 23 13:00:19 2011 +0200
    14.3 @@ -7,7 +7,7 @@
    14.4  
    14.5  theory Conform imports State WellType Exceptions begin
    14.6  
    14.7 -types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
    14.8 +type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
    14.9  
   14.10  definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
   14.11   "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
    15.1 --- a/src/HOL/MicroJava/J/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
    15.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
    15.3 @@ -7,18 +7,23 @@
    15.4  
    15.5  theory Decl imports Type begin
    15.6  
    15.7 -types 
    15.8 +type_synonym 
    15.9    fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
   15.10  
   15.11 +type_synonym
   15.12    sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
   15.13  
   15.14 +type_synonym
   15.15    'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
   15.16  
   15.17 +type_synonym
   15.18    'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
   15.19    -- "class = superclass, fields, methods"
   15.20  
   15.21 +type_synonym
   15.22    'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
   15.23  
   15.24 +type_synonym
   15.25    'c prog  = "'c cdecl list"     -- "program"
   15.26  
   15.27  
    16.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Apr 22 15:57:43 2011 +0200
    16.2 +++ b/src/HOL/MicroJava/J/State.thy	Sat Apr 23 13:00:19 2011 +0200
    16.3 @@ -9,9 +9,10 @@
    16.4  imports TypeRel Value
    16.5  begin
    16.6  
    16.7 -types 
    16.8 +type_synonym 
    16.9    fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
   16.10  
   16.11 +type_synonym
   16.12    obj = "cname \<times> fields'"    -- "class instance with class name and fields"
   16.13  
   16.14  definition obj_ty :: "obj => ty" where
   16.15 @@ -20,11 +21,11 @@
   16.16  definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
   16.17   "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
   16.18  
   16.19 -types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
   16.20 -      locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
   16.21 +type_synonym aheap = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
   16.22 +type_synonym locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
   16.23  
   16.24 -      state  = "aheap \<times> locals"      -- "heap, local parameter including This"
   16.25 -      xstate = "val option \<times> state" -- "state including exception information"
   16.26 +type_synonym state = "aheap \<times> locals"      -- "heap, local parameter including This"
   16.27 +type_synonym xstate = "val option \<times> state" -- "state including exception information"
   16.28  
   16.29  abbreviation (input)
   16.30    heap :: "state => aheap"
    17.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Fri Apr 22 15:57:43 2011 +0200
    17.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Apr 23 13:00:19 2011 +0200
    17.3 @@ -25,7 +25,7 @@
    17.4  \end{itemize}
    17.5  \end{description}
    17.6  *}
    17.7 -types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
    17.8 +type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
    17.9  
   17.10  definition wf_syscls :: "'c prog => bool" where
   17.11  "wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
    18.1 --- a/src/HOL/MicroJava/J/WellType.thy	Fri Apr 22 15:57:43 2011 +0200
    18.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Sat Apr 23 13:00:19 2011 +0200
    18.3 @@ -22,9 +22,8 @@
    18.4  *}
    18.5  
    18.6  text "local variables, including method parameters and This:"
    18.7 -types 
    18.8 -  lenv   = "vname \<rightharpoonup> ty"
    18.9 -  'c env = "'c prog \<times> lenv"
   18.10 +type_synonym lenv = "vname \<rightharpoonup> ty"
   18.11 +type_synonym 'c env = "'c prog \<times> lenv"
   18.12  
   18.13  abbreviation (input)
   18.14    prg :: "'c env => 'c prog"
   18.15 @@ -99,7 +98,7 @@
   18.16  apply auto
   18.17  done
   18.18  
   18.19 -types
   18.20 +type_synonym
   18.21    java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
   18.22  -- "method body with parameter names, local variables, block, result expression."
   18.23  -- "local variables might include This, which is hidden anyway"
    19.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Fri Apr 22 15:57:43 2011 +0200
    19.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Apr 23 13:00:19 2011 +0200
    19.3 @@ -28,13 +28,17 @@
    19.4          | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
    19.5          | Throw                     -- "throw top of stack as exception"
    19.6  
    19.7 -types
    19.8 +type_synonym
    19.9    bytecode = "instr list"
   19.10 +type_synonym
   19.11    exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
   19.12                    -- "start-pc, end-pc, handler-pc, exception type"
   19.13 +type_synonym
   19.14    exception_table = "exception_entry list"
   19.15 +type_synonym
   19.16    jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
   19.17     -- "max stacksize, size of register set, instruction sequence, handler table"
   19.18 +type_synonym
   19.19    jvm_prog = "jvm_method prog" 
   19.20  
   19.21  end
    20.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Fri Apr 22 15:57:43 2011 +0200
    20.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sat Apr 23 13:00:19 2011 +0200
    20.3 @@ -12,11 +12,11 @@
    20.4  begin
    20.5  
    20.6  section {* Frame Stack *}
    20.7 -types
    20.8 - opstack   = "val list"
    20.9 - locvars   = "val list" 
   20.10 - p_count   = nat
   20.11 +type_synonym opstack = "val list"
   20.12 +type_synonym locvars = "val list"
   20.13 +type_synonym p_count = nat
   20.14  
   20.15 +type_synonym
   20.16   frame = "opstack \<times>     
   20.17            locvars \<times>   
   20.18            cname \<times>     
   20.19 @@ -35,7 +35,7 @@
   20.20    "raise_system_xcpt b x \<equiv> raise_if b x None"
   20.21  
   20.22  section {* Runtime State *}
   20.23 -types
   20.24 +type_synonym
   20.25    jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
   20.26  
   20.27  
    21.1 --- a/src/HOL/NSA/HyperDef.thy	Fri Apr 22 15:57:43 2011 +0200
    21.2 +++ b/src/HOL/NSA/HyperDef.thy	Sat Apr 23 13:00:19 2011 +0200
    21.3 @@ -10,7 +10,7 @@
    21.4  imports HyperNat Real
    21.5  begin
    21.6  
    21.7 -types hypreal = "real star"
    21.8 +type_synonym hypreal = "real star"
    21.9  
   21.10  abbreviation
   21.11    hypreal_of_real :: "real => real star" where
    22.1 --- a/src/HOL/NSA/HyperNat.thy	Fri Apr 22 15:57:43 2011 +0200
    22.2 +++ b/src/HOL/NSA/HyperNat.thy	Sat Apr 23 13:00:19 2011 +0200
    22.3 @@ -11,7 +11,7 @@
    22.4  imports StarDef
    22.5  begin
    22.6  
    22.7 -types hypnat = "nat star"
    22.8 +type_synonym hypnat = "nat star"
    22.9  
   22.10  abbreviation
   22.11    hypnat_of_nat :: "nat => nat star" where
    23.1 --- a/src/HOL/NSA/NSComplex.thy	Fri Apr 22 15:57:43 2011 +0200
    23.2 +++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 23 13:00:19 2011 +0200
    23.3 @@ -9,7 +9,7 @@
    23.4  imports Complex NSA
    23.5  begin
    23.6  
    23.7 -types hcomplex = "complex star"
    23.8 +type_synonym hcomplex = "complex star"
    23.9  
   23.10  abbreviation
   23.11    hcomplex_of_complex :: "complex => complex star" where
    24.1 --- a/src/HOL/NanoJava/AxSem.thy	Fri Apr 22 15:57:43 2011 +0200
    24.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sat Apr 23 13:00:19 2011 +0200
    24.3 @@ -6,10 +6,10 @@
    24.4  
    24.5  theory AxSem imports State begin
    24.6  
    24.7 -types assn   = "state => bool"
    24.8 -     vassn   = "val => assn"
    24.9 -      triple = "assn \<times> stmt \<times>  assn"
   24.10 -     etriple = "assn \<times> expr \<times> vassn"
   24.11 +type_synonym assn = "state => bool"
   24.12 +type_synonym vassn = "val => assn"
   24.13 +type_synonym triple = "assn \<times> stmt \<times>  assn"
   24.14 +type_synonym etriple = "assn \<times> expr \<times> vassn"
   24.15  translations
   24.16    (type) "assn" \<leftharpoondown> (type) "state => bool"
   24.17    (type) "vassn" \<leftharpoondown> (type) "val => assn"
    25.1 --- a/src/HOL/NanoJava/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
    25.2 +++ b/src/HOL/NanoJava/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
    25.3 @@ -12,7 +12,7 @@
    25.4    | Class cname  --{* class type *}
    25.5  
    25.6  text{* Field declaration *}
    25.7 -types   fdecl           
    25.8 +type_synonym fdecl           
    25.9          = "fname \<times> ty"
   25.10  
   25.11  record  methd           
   25.12 @@ -22,7 +22,7 @@
   25.13            bdy :: stmt
   25.14  
   25.15  text{* Method declaration *}
   25.16 -types   mdecl
   25.17 +type_synonym mdecl
   25.18          = "mname \<times> methd"
   25.19  
   25.20  record  "class"
   25.21 @@ -31,10 +31,10 @@
   25.22            methods ::"mdecl list"
   25.23  
   25.24  text{* Class declaration *}
   25.25 -types   cdecl
   25.26 +type_synonym cdecl
   25.27          = "cname \<times> class"
   25.28  
   25.29 -types   prog
   25.30 +type_synonym prog
   25.31          = "cdecl list"
   25.32  
   25.33  translations
    26.1 --- a/src/HOL/NanoJava/State.thy	Fri Apr 22 15:57:43 2011 +0200
    26.2 +++ b/src/HOL/NanoJava/State.thy	Sat Apr 23 13:00:19 2011 +0200
    26.3 @@ -17,9 +17,10 @@
    26.4    = Null        --{* null reference *}
    26.5    | Addr loc    --{* address, i.e. location of object *}
    26.6  
    26.7 -types   fields
    26.8 +type_synonym fields
    26.9          = "(fname \<rightharpoonup> val)"
   26.10  
   26.11 +type_synonym
   26.12          obj = "cname \<times> fields"
   26.13  
   26.14  translations
   26.15 @@ -30,8 +31,8 @@
   26.16   "init_vars m == Option.map (\<lambda>T. Null) o m"
   26.17    
   26.18  text {* private: *}
   26.19 -types   heap   = "loc   \<rightharpoonup> obj"
   26.20 -        locals = "vname \<rightharpoonup> val"  
   26.21 +type_synonym heap = "loc   \<rightharpoonup> obj"
   26.22 +type_synonym locals = "vname \<rightharpoonup> val"  
   26.23  
   26.24  text {* private: *}
   26.25  record  state
    27.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Fri Apr 22 15:57:43 2011 +0200
    27.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Apr 23 13:00:19 2011 +0200
    27.3 @@ -19,7 +19,7 @@
    27.4  typedecl key
    27.5  typedecl room
    27.6  
    27.7 -types keycard = "key \<times> key"
    27.8 +type_synonym keycard = "key \<times> key"
    27.9  
   27.10  record state =
   27.11    owns :: "room \<Rightarrow> guest option"
    28.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Apr 22 15:57:43 2011 +0200
    28.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Apr 23 13:00:19 2011 +0200
    28.3 @@ -16,7 +16,7 @@
    28.4                              
    28.5  datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
    28.6  
    28.7 -types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
    28.8 +type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
    28.9  
   28.10  fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
   28.11  where
   28.12 @@ -120,9 +120,8 @@
   28.13  
   28.14  subsection {* IMP *}
   28.15  
   28.16 -types
   28.17 -  var = nat
   28.18 -  state = "int list"
   28.19 +type_synonym var = nat
   28.20 +type_synonym state = "int list"
   28.21  
   28.22  datatype com =
   28.23    Skip |
   28.24 @@ -217,10 +216,9 @@
   28.25  
   28.26  text {* thanks to Elke Salecker *}
   28.27  
   28.28 -types
   28.29 -  vname = nat
   28.30 -  vvalue = int
   28.31 -  var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
   28.32 +type_synonym vname = nat
   28.33 +type_synonym vvalue = int
   28.34 +type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
   28.35  
   28.36  datatype ir_expr = 
   28.37    IrConst vvalue
   28.38 @@ -248,9 +246,8 @@
   28.39  
   28.40  subsection {* Another semantics *}
   28.41  
   28.42 -types
   28.43 -  name = nat --"For simplicity in examples"
   28.44 -  state' = "name \<Rightarrow> nat"
   28.45 +type_synonym name = nat --"For simplicity in examples"
   28.46 +type_synonym state' = "name \<Rightarrow> nat"
   28.47  
   28.48  datatype aexp = N nat | V name | Plus aexp aexp
   28.49  
    29.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Apr 22 15:57:43 2011 +0200
    29.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Apr 23 13:00:19 2011 +0200
    29.3 @@ -6,7 +6,7 @@
    29.4  datatype key = Key0 | Key1 | Key2 | Key3
    29.5  datatype room = Room0
    29.6  
    29.7 -types card = "key * key"
    29.8 +type_synonym card = "key * key"
    29.9  
   29.10  datatype event =
   29.11     Check_in guest room card | Enter guest room card | Exit guest room
    30.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Apr 22 15:57:43 2011 +0200
    30.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Sat Apr 23 13:00:19 2011 +0200
    30.3 @@ -8,9 +8,8 @@
    30.4    In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
    30.5  *}
    30.6  
    30.7 -types
    30.8 -  var = nat
    30.9 -  state = "int list"
   30.10 +type_synonym var = nat
   30.11 +type_synonym state = "int list"
   30.12  
   30.13  datatype com =
   30.14    Skip |
    31.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
    31.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
    31.3 @@ -176,9 +176,8 @@
    31.4  *)
    31.5  subsection {* IMP *}
    31.6  
    31.7 -types
    31.8 -  var = nat
    31.9 -  state = "int list"
   31.10 +type_synonym var = nat
   31.11 +type_synonym state = "int list"
   31.12  
   31.13  datatype com =
   31.14    Skip |
    32.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Apr 22 15:57:43 2011 +0200
    32.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Apr 23 13:00:19 2011 +0200
    32.3 @@ -770,9 +770,8 @@
    32.4  
    32.5  subsection {* IMP *}
    32.6  
    32.7 -types
    32.8 -  var = nat
    32.9 -  state = "int list"
   32.10 +type_synonym var = nat
   32.11 +type_synonym state = "int list"
   32.12  
   32.13  datatype com =
   32.14    Skip |
    33.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
    33.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
    33.3 @@ -110,7 +110,7 @@
    33.4    | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
    33.5  
    33.6  datatype binding = VarB type | TVarB type
    33.7 -types env = "binding list"
    33.8 +type_synonym env = "binding list"
    33.9  
   33.10  primrec is_TVarB :: "binding \<Rightarrow> bool"
   33.11  where
    34.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Apr 22 15:57:43 2011 +0200
    34.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Sat Apr 23 13:00:19 2011 +0200
    34.3 @@ -32,8 +32,7 @@
    34.4  
    34.5  
    34.6  
    34.7 -types
    34.8 -  key = nat
    34.9 +type_synonym key = nat
   34.10  
   34.11  consts
   34.12    all_symmetric :: bool        --{*true if all keys are symmetric*}
    35.1 --- a/src/HOL/UNITY/Comp/Client.thy	Fri Apr 22 15:57:43 2011 +0200
    35.2 +++ b/src/HOL/UNITY/Comp/Client.thy	Sat Apr 23 13:00:19 2011 +0200
    35.3 @@ -7,7 +7,7 @@
    35.4  
    35.5  theory Client imports "../Rename" AllocBase begin
    35.6  
    35.7 -types
    35.8 +type_synonym
    35.9    tokbag = nat     --{*tokbags could be multisets...or any ordered type?*}
   35.10  
   35.11  record state =
    36.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Fri Apr 22 15:57:43 2011 +0200
    36.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Sat Apr 23 13:00:19 2011 +0200
    36.3 @@ -14,7 +14,7 @@
    36.4  
    36.5  (* Variables are names *)
    36.6  datatype name = C | c nat
    36.7 -types state = "name=>int"
    36.8 +type_synonym state = "name=>int"
    36.9  
   36.10  primrec sum  :: "[nat,state]=>int" where
   36.11    (* sum I s = sigma_{i<I}. s (c i) *)
   36.12 @@ -25,7 +25,7 @@
   36.13    "sumj 0 i s = 0"
   36.14  | "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
   36.15    
   36.16 -types command = "(state*state)set"
   36.17 +type_synonym command = "(state*state)set"
   36.18  
   36.19  definition a :: "nat=>command" where
   36.20   "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
    37.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Fri Apr 22 15:57:43 2011 +0200
    37.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Apr 23 13:00:19 2011 +0200
    37.3 @@ -30,7 +30,7 @@
    37.4    "sumj 0 i s = 0"
    37.5  | "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
    37.6    
    37.7 -types command = "(state*state)set"
    37.8 +type_synonym command = "(state*state)set"
    37.9  
   37.10  definition a :: "nat=>command" where
   37.11   "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
    38.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Fri Apr 22 15:57:43 2011 +0200
    38.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Sat Apr 23 13:00:19 2011 +0200
    38.3 @@ -12,8 +12,8 @@
    38.4     In J. Rolim (editor), Parallel and Distributed Processing,
    38.5     Spriner LNCS 1586 (1999), pages 1215-1227.*}
    38.6  
    38.7 -types state = "(vertex*vertex)set"
    38.8 -types command = "vertex=>(state*state)set"
    38.9 +type_synonym state = "(vertex*vertex)set"
   38.10 +type_synonym command = "vertex=>(state*state)set"
   38.11    
   38.12  consts
   38.13    init :: "(vertex*vertex)set"  
    39.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Fri Apr 22 15:57:43 2011 +0200
    39.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sat Apr 23 13:00:19 2011 +0200
    39.3 @@ -7,7 +7,7 @@
    39.4  
    39.5  theory TimerArray imports "../UNITY_Main" begin
    39.6  
    39.7 -types 'a state = "nat * 'a"   (*second component allows new variables*)
    39.8 +type_synonym 'a state = "nat * 'a"   (*second component allows new variables*)
    39.9  
   39.10  definition count :: "'a state => nat"
   39.11    where "count s = fst s"
    40.1 --- a/src/HOL/UNITY/Simple/Channel.thy	Fri Apr 22 15:57:43 2011 +0200
    40.2 +++ b/src/HOL/UNITY/Simple/Channel.thy	Sat Apr 23 13:00:19 2011 +0200
    40.3 @@ -9,7 +9,7 @@
    40.4  
    40.5  theory Channel imports "../UNITY_Main" begin
    40.6  
    40.7 -types state = "nat set"
    40.8 +type_synonym state = "nat set"
    40.9  
   40.10  consts
   40.11    F :: "state program"
    41.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Fri Apr 22 15:57:43 2011 +0200
    41.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Apr 23 13:00:19 2011 +0200
    41.3 @@ -14,7 +14,7 @@
    41.4    u :: bool
    41.5    v :: bool
    41.6  
    41.7 -types command = "(state*state) set"
    41.8 +type_synonym command = "(state*state) set"
    41.9  
   41.10  
   41.11    (** The program for process U **)
    42.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Apr 22 15:57:43 2011 +0200
    42.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Apr 23 13:00:19 2011 +0200
    42.3 @@ -15,7 +15,7 @@
    42.4    Proc. Royal Soc. 426 (1989).
    42.5  *}
    42.6  
    42.7 -types state = "event list"
    42.8 +type_synonym state = "event list"
    42.9  
   42.10    (*The spy MAY say anything he CAN say.  We do not expect him to
   42.11      invent new nonces here, but he can also use NS1.  Common to
    43.1 --- a/src/HOL/UNITY/Simple/Network.thy	Fri Apr 22 15:57:43 2011 +0200
    43.2 +++ b/src/HOL/UNITY/Simple/Network.thy	Sat Apr 23 13:00:19 2011 +0200
    43.3 @@ -15,7 +15,7 @@
    43.4  
    43.5  datatype pname = Aproc | Bproc
    43.6  
    43.7 -types state = "pname * pvar => nat"
    43.8 +type_synonym state = "pname * pvar => nat"
    43.9  
   43.10  locale F_props =
   43.11    fixes F 
    44.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Fri Apr 22 15:57:43 2011 +0200
    44.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Apr 23 13:00:19 2011 +0200
    44.3 @@ -10,7 +10,7 @@
    44.4  
    44.5  typedecl vertex
    44.6  
    44.7 -types    state = "vertex=>bool"
    44.8 +type_synonym state = "vertex=>bool"
    44.9  
   44.10  consts
   44.11    init ::  "vertex"
    45.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Fri Apr 22 15:57:43 2011 +0200
    45.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Sat Apr 23 13:00:19 2011 +0200
    45.3 @@ -10,7 +10,7 @@
    45.4  
    45.5  theory Reachability imports "../Detects" Reach begin
    45.6  
    45.7 -types  edge = "(vertex*vertex)"
    45.8 +type_synonym edge = "vertex * vertex"
    45.9  
   45.10  record state =
   45.11    reach :: "vertex => bool"
    46.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Fri Apr 22 15:57:43 2011 +0200
    46.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Sat Apr 23 13:00:19 2011 +0200
    46.3 @@ -10,9 +10,9 @@
    46.4  imports Word
    46.5  begin
    46.6  
    46.7 -types word32 = "32 word"
    46.8 -types word8 = "8 word"
    46.9 -types byte = word8
   46.10 +type_synonym word32 = "32 word"
   46.11 +type_synonym word8 = "8 word"
   46.12 +type_synonym byte = word8
   46.13  
   46.14  -- "modulus"
   46.15  
    47.1 --- a/src/HOL/ex/CTL.thy	Fri Apr 22 15:57:43 2011 +0200
    47.2 +++ b/src/HOL/ex/CTL.thy	Sat Apr 23 13:00:19 2011 +0200
    47.3 @@ -21,7 +21,7 @@
    47.4  
    47.5  lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
    47.6  
    47.7 -types 'a ctl = "'a set"
    47.8 +type_synonym 'a ctl = "'a set"
    47.9  
   47.10  definition
   47.11    imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where
    48.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri Apr 22 15:57:43 2011 +0200
    48.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Sat Apr 23 13:00:19 2011 +0200
    48.3 @@ -96,7 +96,7 @@
    48.4  
    48.5  subsection {* Colinearity is invariant by rotation *}
    48.6  
    48.7 -types point = "int \<times> int"
    48.8 +type_synonym point = "int \<times> int"
    48.9  
   48.10  definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
   48.11    "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
    49.1 --- a/src/HOL/ex/RPred.thy	Fri Apr 22 15:57:43 2011 +0200
    49.2 +++ b/src/HOL/ex/RPred.thy	Sat Apr 23 13:00:19 2011 +0200
    49.3 @@ -2,7 +2,7 @@
    49.4  imports Quickcheck Random Predicate
    49.5  begin
    49.6  
    49.7 -types 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    49.8 +type_synonym 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    49.9  
   49.10  section {* The RandomPred Monad *}
   49.11  
    50.1 --- a/src/HOL/ex/Records.thy	Fri Apr 22 15:57:43 2011 +0200
    50.2 +++ b/src/HOL/ex/Records.thy	Sat Apr 23 13:00:19 2011 +0200
    50.3 @@ -235,7 +235,7 @@
    50.4  record 'a point'' = point +
    50.5    content :: 'a
    50.6  
    50.7 -types cpoint'' = "colour point''"
    50.8 +type_synonym cpoint'' = "colour point''"
    50.9  
   50.10  
   50.11  
    51.1 --- a/src/HOL/ex/Tree23.thy	Fri Apr 22 15:57:43 2011 +0200
    51.2 +++ b/src/HOL/ex/Tree23.thy	Sat Apr 23 13:00:19 2011 +0200
    51.3 @@ -19,7 +19,7 @@
    51.4  function definitions take a few minutes and can also be seen as stress tests
    51.5  for the function definition facility.  *}
    51.6  
    51.7 -types key = int -- {*for simplicity, should be a type class*}
    51.8 +type_synonym key = int -- {*for simplicity, should be a type class*}
    51.9  
   51.10  datatype ord = LESS | EQUAL | GREATER
   51.11  
    52.1 --- a/src/HOL/ex/Unification.thy	Fri Apr 22 15:57:43 2011 +0200
    52.2 +++ b/src/HOL/ex/Unification.thy	Sat Apr 23 13:00:19 2011 +0200
    52.3 @@ -31,8 +31,7 @@
    52.4    | Const 'a
    52.5    | App "'a trm" "'a trm" (infix "\<cdot>" 60)
    52.6  
    52.7 -types
    52.8 -  'a subst = "('a \<times> 'a trm) list"
    52.9 +type_synonym 'a subst = "('a \<times> 'a trm) list"
   52.10  
   52.11  text {* Applying a substitution to a variable: *}
   52.12  
    53.1 --- a/src/Sequents/Sequents.thy	Fri Apr 22 15:57:43 2011 +0200
    53.2 +++ b/src/Sequents/Sequents.thy	Sat Apr 23 13:00:19 2011 +0200
    53.3 @@ -40,17 +40,15 @@
    53.4   "_SeqO"           :: "o => seqobj"                        ("_")
    53.5   "_SeqId"          :: "'a => seqobj"                       ("$_")
    53.6  
    53.7 -types
    53.8 - single_seqe = "[seq,seqobj] => prop"
    53.9 - single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
   53.10 - two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
   53.11 - two_seqe    = "[seq, seq] => prop"
   53.12 - three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   53.13 - three_seqe  = "[seq, seq, seq] => prop"
   53.14 - four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   53.15 - four_seqe   = "[seq, seq, seq, seq] => prop"
   53.16 -
   53.17 - sequence_name = "seq'=>seq'"
   53.18 +type_synonym single_seqe = "[seq,seqobj] => prop"
   53.19 +type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
   53.20 +type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
   53.21 +type_synonym two_seqe = "[seq, seq] => prop"
   53.22 +type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   53.23 +type_synonym three_seqe = "[seq, seq, seq] => prop"
   53.24 +type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   53.25 +type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
   53.26 +type_synonym sequence_name = "seq'=>seq'"
   53.27  
   53.28  
   53.29  syntax