Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
streamlined specification of included theories
authoroheimb
Thu, 08 Jan 1998 18:03:36 +0100
changeset 4531 20a7fddb706a
parent 4530 ac1821645636
child 4532 006e5572aca8
streamlined specification of included theories
src/HOL/Quot/NPAIR.thy file | annotate | diff | comparison | revisions
src/HOL/Quot/PER.thy file | annotate | diff | comparison | revisions 
--- 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 *)
 
--- 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) |}
isabelle