--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Type_Class.thy Tue May 31 12:24:43 2016 +0200
@@ -0,0 +1,31 @@
+(* Title: HOL/Corec_Examples/Tests/Type_Class.thy
+ Author: Andreas Lochbihler, ETH Zuerich
+ Author: Jasmin Blanchette, Inria, LORIA, MPII
+ Copyright 2016
+
+Tests type class instances as friends.
+*)
+
+section \<open>Tests Type Class Instances as Friends\<close>
+
+theory Type_Class
+imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
+begin
+
+instantiation stream :: (plus) plus
+begin
+
+definition plus_stream where "plus_stream s1 s2 = smap (\<lambda>(x, y). x + y) (sproduct s1 s2)"
+
+instance ..
+
+end
+
+friend_of_corec plus (* :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" *) where
+ "s1 + s2 = SCons (shd s1 + shd s2) (stl s1 + stl s2)"
+ sorry
+
+corec ff :: "('a::plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+ "ff xs ys = SCons (shd xs + shd ys) (ff (stl xs) ys) + SCons (shd xs) (ff xs (stl ys))"
+
+end
--- a/src/HOL/ROOT Tue May 31 11:54:45 2016 +0200
+++ b/src/HOL/ROOT Tue May 31 12:24:43 2016 +0200
@@ -832,6 +832,7 @@
"Tests/Small_Concrete"
"Tests/Stream_Friends"
"Tests/TLList_Friends"
+ "Tests/Type_Class"
session "HOL-Word" (main) in Word = HOL +
theories Word