# HG changeset patch
# User wenzelm
# Date 1258294411 -3600
# Node ID bec342db1bf4059910dd8323923858d86274085a
# Parent  f06fe9c2152ddd7256e2f185d82b9ed74bc2f0aa
eliminated obsolete CVS Ids;
tuned headers;

diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-datatype/Brackin.thy
--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy	Sun Nov 15 15:13:31 2009 +0100
@@ -1,13 +1,10 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
-    ID:         $Id$
+
+A couple from Steve Brackin's work.
 *)
 
 theory Brackin imports Main begin
 
-(* ------------------------------------------------------------------------- *)
-(* A couple from Steve Brackin's work.                                       *)
-(* ------------------------------------------------------------------------- *)
-
 datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
                 X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
                 X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-datatype/Instructions.thy
--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-datatype/Instructions.thy	Sun Nov 15 15:13:31 2009 +0100
@@ -1,13 +1,10 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/Instructions.thy
-    ID:         $Id$
+
+Example from Konrad: 68000 instruction set.
 *)
 
 theory Instructions imports Main begin
 
-(* ------------------------------------------------------------------------- *)
-(* Example from Konrad: 68000 instruction set.                               *)
-(* ------------------------------------------------------------------------- *)
-
 datatype Size = Byte | Word | Long
 
 datatype DataRegister
diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-datatype/SML.thy
--- a/Admin/Benchmarks/HOL-datatype/SML.thy	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy	Sun Nov 15 15:13:31 2009 +0100
@@ -1,13 +1,10 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/SML.thy
-    ID:         $Id$
+
+Example from Myra: part of the syntax of SML.
 *)
 
 theory SML imports Main begin
 
-(* ------------------------------------------------------------------------- *)
-(* Example from Myra: part of the syntax of SML.                             *)
-(* ------------------------------------------------------------------------- *)
-
 datatype
   string = EMPTY_STRING | CONS_STRING nat string
 
diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-datatype/Verilog.thy
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-datatype/Verilog.thy	Sun Nov 15 15:13:31 2009 +0100
@@ -1,13 +1,10 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
-    ID:         $Id$
+
+Example from Daryl: a Verilog grammar.
 *)
 
 theory Verilog imports Main begin
 
-(* ------------------------------------------------------------------------- *)
-(* Example from Daryl: a Verilog grammar.                                    *)
-(* ------------------------------------------------------------------------- *)
-
 datatype
   Source_text
      = module string "string list" "Module_item list"
diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-record/ROOT.ML
--- a/Admin/Benchmarks/HOL-record/ROOT.ML	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-record/ROOT.ML	Sun Nov 15 15:13:31 2009 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Admin/Benchmarks/HOL-record/ROOT.ML
 
-Some benchmark on large record
+Some benchmark on large record.
 *)
 
 val tests = ["RecordBenchmark"];
diff -r f06fe9c2152d -r bec342db1bf4 Admin/Benchmarks/HOL-record/RecordBenchmark.thy
--- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Sun Nov 15 13:06:42 2009 +0100
+++ b/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Sun Nov 15 15:13:31 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Admin/Benchmarks/HOL-record/RecordBenchmark.thy
-    Author:     Norbert Schirmer
-                DFKI
+    Author:     Norbert Schirmer, DFKI
 *)
 
 header {* Benchmark for large record *}
@@ -393,5 +392,4 @@
   done
 
 
-
 end
\ No newline at end of file