1(*  Title:      HOL/Corec_Examples/Tests/Merge_C.thy
2    Author:     Aymeric Bouzy, Ecole polytechnique
3    Author:     Jasmin Blanchette, Inria, LORIA, MPII
4    Copyright   2015, 2016
5
6Tests theory merges.
7*)
8
9section \<open>Tests Theory Merges\<close>
10
11theory Merge_C
12imports Merge_A
13begin
14
15consts fc :: "'a ta \<Rightarrow> 'a ta"
16consts gc :: "'a ta \<Rightarrow> 'a ta"
17
18friend_of_corec fc :: "'a ta \<Rightarrow> 'a ta" where
19  "fc t = Ca (sa1 t) (sa2 t)"
20  sorry
21
22friend_of_corec gb :: "'a ta \<Rightarrow> 'a ta" where
23  "gb t = Ca (sa1 t) (sa2 t)"
24  sorry
25
26friend_of_corec gc :: "'a ta \<Rightarrow> 'a ta" where
27  "gc t = Ca (sa1 t) (sa2 t)"
28  sorry
29
30end
31