# HG changeset patch
# User huffman
# Date 1240358864 25200
# Node ID 96d053e00ec013fbd55484ec8a65730d6376738f
# Parent  fbdefa2196fa50f300c3e34cc15470cdda579efd
add more examples to Domain_ex.thy

diff -r fbdefa2196fa -r 96d053e00ec0 src/HOLCF/ex/Domain_ex.thy
--- a/src/HOLCF/ex/Domain_ex.thy	Tue Apr 21 17:02:48 2009 -0700
+++ b/src/HOLCF/ex/Domain_ex.thy	Tue Apr 21 17:07:44 2009 -0700
@@ -203,4 +203,19 @@
   -- "Tactic failed."
 *)
 
+text {* Declaring class constraints on the LHS is currently broken. *}
+(*
+domain ('a::cpo) box = Box (lazy 'a)
+  -- "Malformed YXML encoding: multiple results"
+*)
+
+text {*
+  Class constraints on the RHS are not supported yet.  This feature is
+  planned to replace the old-style LHS class constraints.
+*}
+(*
+domain 'a box = Box (lazy "'a::cpo")
+  -- {* Inconsistent sort constraint for type variable "'a" *}
+*)
+
 end