# HG changeset patch
# User oheimb
# Date 884279016 -3600
# Node ID 20a7fddb706a0b2354b8c48a55b56ab7df2b6c59
# Parent  ac1821645636bc4639e798692707192220fbf3d7
streamlined specification of included theories

diff -r ac1821645636 -r 20a7fddb706a src/HOL/Quot/NPAIR.thy
--- a/src/HOL/Quot/NPAIR.thy	Thu Jan 08 18:00:42 1998 +0100
+++ b/src/HOL/Quot/NPAIR.thy	Thu Jan 08 18:03:36 1998 +0100
@@ -6,7 +6,7 @@
 Example: define a PER on pairs of natural numbers (with embedding)
 
 *)
-NPAIR = Arith + Prod + PER +  (* representation for rational numbers *)
+NPAIR = PER + Arith + (* representation for rational numbers *)
 
 types np = "(nat * nat)" (* is needed for datatype *)
 
diff -r ac1821645636 -r 20a7fddb706a src/HOL/Quot/PER.thy
--- a/src/HOL/Quot/PER.thy	Thu Jan 08 18:00:42 1998 +0100
+++ b/src/HOL/Quot/PER.thy	Thu Jan 08 18:03:36 1998 +0100
@@ -6,7 +6,7 @@
 instances for per - makes PER higher order
 *)
 
-PER = PER0 +  (* instance for per *)
+PER = PER0 + (* instance for per *)
 
 instance fun  :: (per,per)per   
 {| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}