--- 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"
--- 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
--- 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")
--- 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}"
--- 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"
--- 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*}
--- 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
--- 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
--- 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>
--- 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"
--- 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"
--- 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"
--- 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"
--- 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'))"
--- 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"
--- 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"
--- 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)"
--- 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"
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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 |
--- 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 |
--- 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 |
--- 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
--- 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*}
--- 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 =
--- 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)}"
--- 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}"
--- 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"
--- 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"
--- 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"
--- 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 **)
--- 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
--- 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
--- 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"
--- 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"
--- 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"
--- 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
--- 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).
--- 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 *}
--- 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''"
--- 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
--- 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: *}
--- 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