# HG changeset patch
# User wenzelm
# Date 1322665398 -3600
# Node ID d2567e55af83db8ebcef025f8d54334e332a9bd8
# Parent  d1e716cc3b8462c19c85251550db4192efcce3b0
tuned header;

diff -r d1e716cc3b84 -r d2567e55af83 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Nov 30 12:09:29 2011 +0100
+++ b/src/HOL/Library/Saturated.thy	Wed Nov 30 16:03:18 2011 +0100
@@ -1,6 +1,8 @@
-(* Author: Brian Huffman *)
-(* Author: Peter Gammie *)
-(* Author: Florian Haftmann *)
+(*  Title:      HOL/Library/Saturated.thy
+    Author:     Brian Huffman
+    Author:     Peter Gammie
+    Author:     Florian Haftmann
+*)
 
 header {* Saturated arithmetic *}