1(*  Title:      HOL/Corec_Examples/Tests/Merge_B.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_B
12imports Merge_A
13begin
14
15consts fb :: "'a ta \<Rightarrow> 'a ta"
16consts gb :: "'a ta \<Rightarrow> 'a ta"
17
18friend_of_corec fb :: "'a ta \<Rightarrow> 'a ta" where
19  "fb 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
26end
27