# HG changeset patch
# User blanchet
# Date 1464690283 -7200
# Node ID 3e79279c10ca0032d9173bed0edec29aa4bc7274
# Parent  d5974697765bb20fcfb4c6b167988748b03f046e
added test

diff -r d5974697765b -r 3e79279c10ca src/HOL/Corec_Examples/Tests/Type_Class.thy
--- /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
diff -r d5974697765b -r 3e79279c10ca src/HOL/ROOT
--- 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