# HG changeset patch
# User bulwahn
# Date 1301477572 -7200
# Node ID 392fd6c4669c8a5c389e2c79bf9498fe41e2f1aa
# Parent  00899500c6ca4978f7f4e1ca4d41bfa77934dd64
renewing specifications in HOL: replacing types by type_synonym

diff -r 00899500c6ca -r 392fd6c4669c src/HOL/DSequence.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Datatype.thy
--- 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))"
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Lazy_Sequence.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Map.thy
--- 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)
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/New_DSequence.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/New_Random_Sequence.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Quickcheck.thy
--- 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)"
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Random.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Random_Sequence.thy
--- 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
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Set.thy
--- 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"
diff -r 00899500c6ca -r 392fd6c4669c src/HOL/String.thy
--- 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"    ("_")