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