# HG changeset patch
# User wenzelm
# Date 1117487278 -7200
# Node ID 8d453f906e43a502b57383bbcf9e1b9fdc3b1ad1
# Parent  692fe6595755913e7152ed5d8e924157f76ca99a
tuned;

diff -r 692fe6595755 -r 8d453f906e43 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon May 30 16:32:47 2005 +0200
+++ b/src/HOL/Record.thy	Mon May 30 23:07:58 2005 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Record.thy
     ID:         $Id$
-    Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
+    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
 *)
 
 theory Record
@@ -58,8 +58,8 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
 
-use "Tools/record_package.ML";
-setup RecordPackage.setup;
+use "Tools/record_package.ML"
+setup RecordPackage.setup
 
 end