--- 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 |
--- 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
--- 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
--- 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"
--- 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"];
--- 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