# HG changeset patch
# User huffman
# Date 1200339352 -3600
# Node ID 695a9d88d697d23961e34bc3adaa21644e971020
# Parent  2179c66612189f9780a0a0fd97d2b380fefc92ec
new-style instantiation proof for unit :: po

diff -r 2179c6661218 -r 695a9d88d697 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:28:59 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:35:52 2008 +0100
@@ -15,17 +15,16 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instantiation unit :: sq_ord
+instantiation unit :: po
 begin
 
 definition
   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
 
-instance ..
-end
+instance
+by intro_classes simp_all
 
-instance unit :: po
-by intro_classes simp_all
+end
 
 instance unit :: finite_po ..