# HG changeset patch
# User huffman
# Date 1294507852 28800
# Node ID 0fa9629aa3992887976de7ac2561403cfb94e16a
# Parent  0e4f6cf20cdf5c2c884550518817c0d0ecb48fb3
types -> type_synonym

diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/FOCUS/Buffer.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -33,11 +33,16 @@
 
   State = Sd D | Snil ("\<currency>")
 
-types
-
+type_synonym
   SPF11         = "M fstream \<rightarrow> D fstream"
+
+type_synonym
   SPEC11        = "SPF11 set"
+
+type_synonym
   SPSF11        = "State \<Rightarrow> SPF11"
+
+type_synonym
   SPECS11       = "SPSF11 set"
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -14,7 +14,7 @@
 
 default_sort type
 
-types 'a fstream = "'a lift stream"
+type_synonym 'a fstream = "'a lift stream"
 
 definition
   fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -12,7 +12,7 @@
 
 default_sort type
 
-types 'a fstream = "('a lift) stream"
+type_synonym 'a fstream = "('a lift) stream"
 
 definition
   fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999) where
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -13,7 +13,7 @@
   the correctness of the Hoare rule for while-loops.
 *}
 
-types assn = "state => bool"
+type_synonym assn = "state => bool"
 
 definition
   hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports IOA Action
 begin
 
-types
+type_synonym
   'm env_state = bool   -- {* give next bit to system *}
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports Sender Receiver Abschannel
 begin
 
-types
+type_synonym
   'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
   (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
 
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports Sender Receiver Abschannel_finite
 begin
 
-types
+type_synonym
   'm impl_fin_state
     = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-types
+type_synonym
   'msg packet = "bool * 'msg"
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports IOA Action Lemmas
 begin
 
-types
+type_synonym
   'm receiver_state = "'m list * bool"  -- {* messages, mode *}
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports IOA Action Lemmas
 begin
 
-types
+type_synonym
   'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports Sender Receiver Abschannel
 begin
 
-types 'm impl_state
+type_synonym 'm impl_state
   = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
   (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
 
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/NTP/Packet.thy
--- a/src/HOL/HOLCF/IOA/NTP/Packet.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -6,7 +6,7 @@
 imports Multiset
 begin
 
-types
+type_synonym
   'msg packet = "bool * 'msg"
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports IOA Action
 begin
 
-types
+type_synonym
 
 'm receiver_state
 = "'m list * bool multiset * 'm packet multiset * bool * bool"
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports IOA Action
 begin
 
-types
+type_synonym
 'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
 (*                messages   #sent           #received      header  mode *)
 
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/Asig.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-types
+type_synonym
   'a signature = "('a set * 'a set * 'a set)"
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,8 +10,10 @@
 
 default_sort type
 
-types
+type_synonym
   ('a, 's) transition = "'s * 'a * 's"
+
+type_synonym
   ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
 
 consts
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,7 +10,7 @@
 
 default_sort type
 
-types
+type_synonym
   ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
 
 definition
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,7 +10,7 @@
 
 default_sort type
 
-types
+type_synonym
   'a predicate = "'a => bool"
 
 consts
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,7 +10,7 @@
 
 default_sort type
 
-types 'a Seq = "'a lift seq"
+type_synonym 'a Seq = "'a lift seq"
 
 consts
 
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,7 +10,7 @@
 
 default_sort type
 
-types
+type_synonym
   'a temporal = "'a Seq predicate"
 
 
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,9 +10,13 @@
 
 default_sort type
 
-types
+type_synonym
   ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
+
+type_synonym
   ('a, 's) step_pred = "('a option,'s)transition predicate"
+
+type_synonym
   's state_pred      = "'s predicate"
 
 consts
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,13 +10,22 @@
 
 default_sort type
 
-types
+type_synonym
    ('a,'s)pairs            =    "('a * 's) Seq"
+
+type_synonym
    ('a,'s)execution        =    "'s * ('a,'s)pairs"
+
+type_synonym
    'a trace                =    "'a Seq"
 
+type_synonym
    ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
+
+type_synonym
    'a schedule_module      = "'a trace set * 'a signature"
+
+type_synonym
    'a trace_module         = "'a trace set * 'a signature"
 
 consts
diff -r 0e4f6cf20cdf -r 0fa9629aa399 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -172,7 +172,7 @@
 
 subsection {* Pattern combinators for data constructors *}
 
-types ('a, 'b) pat = "'a \<rightarrow> 'b match"
+type_synonym ('a, 'b) pat = "'a \<rightarrow> 'b match"
 
 definition
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where