Merge master into improvement/more-descriptive-val-morphism-names

input-output-hk · Oct 3, 2023 · ad9ea0b · ad9ea0b
2 parents 07e3bac + d4531ec
commit ad9ea0b
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/Thorn_Calculus-Derived-Channels-Synchronous.thy b/src/Thorn_Calculus-Derived-Channels-Synchronous.thy
@@ -11,7 +11,10 @@ theory "Thorn_Calculus-Derived-Channels-Synchronous"
 begin
 
 typedef 'a sync_channel = "UNIV :: 'a channel channel set"
-  using UNIV_witness .
+  morphisms sync_channel_to_nested_channel sync_channel_from_nested_channel ..
+
+instance sync_channel :: (type) embeddable
+  by standard (meson sync_channel_to_nested_channel_inject ex_inj inj_def)
 
 lift_definition
   sync_send :: "'a sync_channel \<Rightarrow> 'a \<Rightarrow> process \<Rightarrow> process"