src/HOLCF/Cprod1.thy

--- a/src/HOLCF/Cprod1.thy	Fri Mar 04 18:53:46 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOLCF/Cprod1.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-
-Partial ordering for cartesian product of HOL theory prod.thy
-*)
-
-Cprod1 = Cfun3 +
-
-default cpo
-
-instance "*"::(sq_ord,sq_ord)sq_ord 
-
-defs
-
-  less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
-
-end