--- a/src/HOL/DSequence.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/DSequence.thy Wed Mar 30 11:32:52 2011 +0200
@@ -7,7 +7,7 @@
imports Lazy_Sequence Code_Numeral
begin
-types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
+type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
definition empty :: "'a dseq"
where
--- a/src/HOL/Datatype.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Datatype.thy Wed Mar 30 11:32:52 2011 +0200
@@ -28,8 +28,8 @@
text{*Datatypes will be represented by sets of type @{text node}*}
-types 'a item = "('a, unit) node set"
- ('a, 'b) dtree = "('a, 'b) node set"
+type_synonym 'a item = "('a, unit) node set"
+type_synonym ('a, 'b) dtree = "('a, 'b) node set"
consts
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
--- a/src/HOL/Lazy_Sequence.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Lazy_Sequence.thy Wed Mar 30 11:32:52 2011 +0200
@@ -208,7 +208,7 @@
subsection {* With Hit Bound Value *}
text {* assuming in negative context *}
-types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
+type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
definition hit_bound :: "'a hit_bound_lazy_sequence"
where
--- a/src/HOL/Map.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Map.thy Wed Mar 30 11:32:52 2011 +0200
@@ -11,7 +11,7 @@
imports List
begin
-types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
+type_synonym ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
type_notation (xsymbols)
"map" (infixr "\<rightharpoonup>" 0)
--- a/src/HOL/New_DSequence.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/New_DSequence.thy Wed Mar 30 11:32:52 2011 +0200
@@ -9,7 +9,7 @@
subsection {* Positive Depth-Limited Sequence *}
-types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
+type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
definition pos_empty :: "'a pos_dseq"
where
@@ -49,7 +49,7 @@
subsection {* Negative Depth-Limited Sequence *}
-types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
+type_synonym 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
definition neg_empty :: "'a neg_dseq"
where
--- a/src/HOL/New_Random_Sequence.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/New_Random_Sequence.thy Wed Mar 30 11:32:52 2011 +0200
@@ -5,8 +5,8 @@
imports Quickcheck New_DSequence
begin
-types 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
-types 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
+type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
+type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
definition pos_empty :: "'a pos_random_dseq"
where
--- a/src/HOL/Quickcheck.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Quickcheck.thy Wed Mar 30 11:32:52 2011 +0200
@@ -164,7 +164,7 @@
in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
unfolding iter_def iter'.simps[of _ nrandom] ..
-types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
definition empty :: "'a randompred"
where "empty = Pair (bot_class.bot)"
--- a/src/HOL/Random.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Random.thy Wed Mar 30 11:32:52 2011 +0200
@@ -25,7 +25,7 @@
subsection {* Random seeds *}
-types seed = "code_numeral \<times> code_numeral"
+type_synonym seed = "code_numeral \<times> code_numeral"
primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
"next (v, w) = (let
--- a/src/HOL/Random_Sequence.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Random_Sequence.thy Wed Mar 30 11:32:52 2011 +0200
@@ -5,7 +5,7 @@
imports Quickcheck DSequence
begin
-types 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
+type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
definition empty :: "'a random_dseq"
where
--- a/src/HOL/Set.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Set.thy Wed Mar 30 11:32:52 2011 +0200
@@ -8,7 +8,7 @@
subsection {* Sets as predicates *}
-types 'a set = "'a \<Rightarrow> bool"
+type_synonym 'a set = "'a \<Rightarrow> bool"
definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
"Collect P = P"
--- a/src/HOL/String.thy Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/String.thy Wed Mar 30 11:32:52 2011 +0200
@@ -74,7 +74,7 @@
subsection {* Strings *}
-types string = "char list"
+type_synonym string = "char list"
syntax
"_String" :: "xstr => string" ("_")