# 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\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) -use "Tools/record_package.ML"; -setup RecordPackage.setup; +use "Tools/record_package.ML" +setup RecordPackage.setup end