# HG changeset patch
# User huffman
# Date 1287758674 25200
# Node ID d57357cda8bb89797f1d22445079de579ed66842
# Parent  8adc57fb8454c99e3556894b5e100f20e571fa53
direct instantiation unit :: discrete_cpo

diff -r 8adc57fb8454 -r d57357cda8bb src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Fri Oct 22 06:58:45 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Fri Oct 22 07:44:34 2010 -0700
@@ -12,17 +12,16 @@
 
 subsection {* Unit type is a pcpo *}
 
-instantiation unit :: below
+instantiation unit :: discrete_cpo
 begin
 
 definition
   below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
 
-instance ..
-end
+instance proof
+qed simp
 
-instance unit :: discrete_cpo
-by intro_classes simp
+end
 
 instance unit :: pcpo
 by intro_classes simp