of course it should use Main
authorpaulson
Thu, 04 May 2000 15:16:46 +0200
changeset 8793 a735b1e74f3a
parent 8792 59a4b5e6a591
child 8794 6b524f8c2a2c
of course it should use Main
src/HOL/Quot/NPAIR.thy
--- a/src/HOL/Quot/NPAIR.thy	Thu May 04 15:16:18 2000 +0200
+++ b/src/HOL/Quot/NPAIR.thy	Thu May 04 15:16:46 2000 +0200
@@ -6,7 +6,7 @@
 Example: define a PER on pairs of natural numbers (with embedding)
 
 *)
-NPAIR = PER + Datatype + (* representation for rational numbers *)
+NPAIR = PER + Main + (* representation for rational numbers *)
 
 datatype NP = abs_NP "(nat * nat)"