--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *)
--- 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 *)
--- 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
--- 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
--- 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
--- 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 *)
--- 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
--- 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"
--- 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 *)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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