# HG changeset patch
# User nipkow
# Date 864372035 -7200
# Node ID 0ceaad3c3f528bbd555073d827b905087143f509
# Parent  992a25b24d0d20909e5dd10a0501f89a28f863f8
Base theory is now Arith, not Nat. (because all datatypes now require Arith).

diff -r 992a25b24d0d -r 0ceaad3c3f52 src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Fri May 23 09:18:06 1997 +0200
+++ b/src/HOLCF/Porder0.thy	Fri May 23 09:20:35 1997 +0200
@@ -7,11 +7,11 @@
 
 *)
 
-Porder0 = Nat +
+Porder0 = Arith +
 
 (* first the global constant for HOLCF type classes *)
 consts
-  "less"        :: "['a,'a] => bool"
+  less        :: "['a,'a] => bool"
 
 axclass po < term
         (* class axioms: *)