Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/abstract/Factor.thy
changeset 35849 b5522b51cb1e
parent 21423 6cdd0589aa73 
--- a/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Factorisation within a factorial domain
-    $Id$
-    Author: Clemens Ballarin, started 25 November 1997
+(*  Author: Clemens Ballarin, started 25 November 1997
+
+Factorisation within a factorial domain.
 *)
 
-theory Factor imports Ring2 begin
+theory Factor
+imports Ring2
+begin
 
 definition
   Factorisation :: "['a::ring, 'a list, 'a] => bool" where
isabelle