# HG changeset patch
# User wenzelm
# Date 935744071 -7200
# Node ID 776d888472aa65aa2cb75ada0e13290fed6e2219
# Parent  79e911c0c7d19e9a777c78607eb96c34f1988236
better timing information;

diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/Brackin.thy
--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy	Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
 *)
 
-Brackin = Main +
+theory Brackin = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* A couple from Steve Brackin's work.                                       *)
@@ -16,31 +16,31 @@
 datatype  
   ('a, 'b, 'c) TY1 =
       NoF__
-    | Fk__ 'a (('a, 'b, 'c) TY2)
+    | Fk__ 'a "('a, 'b, 'c) TY2"
 and
   ('a, 'b, 'c) TY2 =
       Ta__ bool
     | Td__ bool
-    | Tf__ (('a, 'b, 'c) TY1)
+    | Tf__ "('a, 'b, 'c) TY1"
     | Tk__ bool
     | Tp__ bool
-    | App__ 'a (('a, 'b, 'c) TY1) (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY3)
-    | Pair__ (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY2)
+    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
 and
   ('a, 'b, 'c) TY3 =
       NoS__
-    | Fresh__ (('a, 'b, 'c) TY2)
+    | Fresh__ "('a, 'b, 'c) TY2"
     | Trustworthy__ 'a
     | PrivateKey__ 'a 'b 'c
     | PublicKey__ 'a 'b 'c
-    | Conveyed__ 'a (('a, 'b, 'c) TY2)
-    | Possesses__ 'a (('a, 'b, 'c) TY2)
-    | Received__ 'a (('a, 'b, 'c) TY2)
-    | Recognizes__ 'a (('a, 'b, 'c) TY2)
-    | NeverMalFromSelf__ 'a 'b (('a, 'b, 'c) TY2)
-    | Sends__ 'a (('a, 'b, 'c) TY2) 'b
-    | SharedSecret__ 'a (('a, 'b, 'c) TY2) 'b
-    | Believes__ 'a (('a, 'b, 'c) TY3)
-    | And__ (('a, 'b, 'c) TY3) (('a, 'b, 'c) TY3)
+    | Conveyed__ 'a "('a, 'b, 'c) TY2"
+    | Possesses__ 'a "('a, 'b, 'c) TY2"
+    | Received__ 'a "('a, 'b, 'c) TY2"
+    | Recognizes__ 'a "('a, 'b, 'c) TY2"
+    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
+    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
+    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
+    | Believes__ 'a "('a, 'b, 'c) TY3"
+    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
 
 end
diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/Instructions.thy
--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Instructions.thy	Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
 *)
 
-Instructions = Main +
+theory Instructions = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Konrad: 68000 instruction set.                               *)
@@ -117,8 +117,8 @@
     | MOVEtoUSP AddressingMode
     | MOVEfromUSP AddressingMode
     | MOVEA Size AddressingMode AddressRegister
-    | MOVEMto Size AddressingMode (DataOrAddressRegister list)
-    | MOVEMfrom Size (DataOrAddressRegister list) AddressingMode
+    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
+    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
     | MOVEP Size AddressingMode AddressingMode
     | MOVEQ nat DataRegister
     | MULS AddressingMode DataRegister
diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Aug 27 10:54:31 1999 +0200
@@ -1,10 +1,16 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
+(*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     ID:         $Id$
 
 Some rather large datatype examples (from John Harrison).
 *)
 
-time_use_thy "Brackin";
-time_use_thy "Instructions";
-time_use_thy "SML";
-time_use_thy "Verilog";
+val tests = ["Brackin", "Instructions", "SML", "Verilog"];
+
+set Toplevel.trace;
+
+warning "\nset quick_and_dirty\n"; set quick_and_dirty;
+seq time_use_thy tests;
+
+warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
+seq remove_thy tests;
+seq time_use_thy tests;
diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/SML.thy
--- a/Admin/Benchmarks/HOL-datatype/SML.thy	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy	Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
 *)
 
-SML = Main +
+theory SML = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Myra: part of the syntax of SML.                             *)
@@ -30,44 +30,44 @@
    label = LABEL string
 
 datatype
-  'a nonemptylist = Head_and_tail 'a ('a list)
+  'a nonemptylist = Head_and_tail 'a "'a list"
 
 datatype
-  'a long = BASE 'a | QUALIFIED strid ('a long)
+  'a long = BASE 'a | QUALIFIED strid "'a long"
 
 datatype
    atpat_e = WILDCARDatpat_e
            | SCONatpat_e scon
            | VARatpat_e var
-           | CONatpat_e (con long)
-           | EXCONatpat_e (excon long)
-           | RECORDatpat_e (patrow_e option)
+           | CONatpat_e "con long"
+           | EXCONatpat_e "excon long"
+           | RECORDatpat_e "patrow_e option"
            | PARatpat_e pat_e
 and
    patrow_e = DOTDOTDOT_e
-            | PATROW_e label pat_e (patrow_e option)
+            | PATROW_e label pat_e "patrow_e option"
 and
    pat_e = ATPATpat_e atpat_e
-         | CONpat_e (con long) atpat_e
-         | EXCONpat_e (excon long) atpat_e
+         | CONpat_e "con long" atpat_e
+         | EXCONpat_e "excon long" atpat_e
          | LAYEREDpat_e var pat_e
 and
-   conbind_e = CONBIND_e con (conbind_e option)
+   conbind_e = CONBIND_e con "conbind_e option"
 and
-   datbind_e = DATBIND_e conbind_e (datbind_e option)
+   datbind_e = DATBIND_e conbind_e "datbind_e option"
 and
-   exbind_e = EXBIND1_e excon (exbind_e option)
-            | EXBIND2_e excon (excon long) (exbind_e option)
+   exbind_e = EXBIND1_e excon "exbind_e option"
+            | EXBIND2_e excon "excon long" "exbind_e option"
 and
    atexp_e = SCONatexp_e scon
-           | VARatexp_e (var long)
-           | CONatexp_e (con long)
-           | EXCONatexp_e (excon long)
-           | RECORDatexp_e (exprow_e option)
+           | VARatexp_e "var long"
+           | CONatexp_e "con long"
+           | EXCONatexp_e "excon long"
+           | RECORDatexp_e "exprow_e option"
            | LETatexp_e dec_e exp_e
            | PARatexp_e exp_e
 and
-   exprow_e = EXPROW_e label exp_e (exprow_e option)
+   exprow_e = EXPROW_e label exp_e "exprow_e option"
 and
    exp_e = ATEXPexp_e atexp_e
          | APPexp_e exp_e atexp_e
@@ -75,7 +75,7 @@
          | RAISEexp_e exp_e
          | FNexp_e match_e
 and
-   match_e = MATCH_e mrule_e (match_e option)
+   match_e = MATCH_e mrule_e "match_e option"
 and
    mrule_e = MRULE_e pat_e exp_e
 and
@@ -84,11 +84,11 @@
          | ABSTYPEdec_e datbind_e dec_e
          | EXCEPTdec_e exbind_e
          | LOCALdec_e dec_e dec_e
-         | OPENdec_e ((strid long) nonemptylist)
+         | OPENdec_e "strid long nonemptylist"
          | EMPTYdec_e
          | SEQdec_e dec_e dec_e
 and
-   valbind_e = PLAINvalbind_e pat_e exp_e (valbind_e option)
+   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
              | RECvalbind_e valbind_e
 
 end
diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/Verilog.thy
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Verilog.thy	Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
 *)
 
-Verilog = Main +
+theory Verilog = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Daryl: a Verilog grammar.                                    *)
@@ -10,7 +10,7 @@
 
 datatype
   Source_text
-     = module string (string list) (Module_item list)
+     = module string "string list" "Module_item list"
      | Source_textMeta string
 and
   Module_item
@@ -21,10 +21,10 @@
      | Module_itemMeta string
 and
   Declaration
-     = reg_declaration (Range option) (string list)
-     | net_declaration (Range option) (string list)
-     | input_declaration (Range option) (string list)
-     | output_declaration (Range option) (string list)
+     = reg_declaration "Range option" "string list"
+     | net_declaration "Range option" "string list"
+     | input_declaration "Range option" "string list"
+     | output_declaration "Range option" "string list"
      | DeclarationMeta string
 and
   Range = range Expression Expression | RangeMeta string
@@ -34,15 +34,15 @@
      | blocking_assignment Lvalue Expression
      | non_blocking_assignment Lvalue Expression
      | conditional_statement
-          Expression Statement_or_null (Statement_or_null option)
-     | case_statement Expression (Case_item list)
+          Expression Statement_or_null "Statement_or_null option"
+     | case_statement Expression "Case_item list"
      | while_loop Expression Statement
      | repeat_loop Expression Statement
      | for_loop
           Lvalue Expression Expression Lvalue Expression Statement
      | forever_loop Statement
      | disable string
-     | seq_block (string option) (Statement list)
+     | seq_block "string option" "Statement list"
      | StatementMeta string
 and
   Statement_or_null
@@ -55,7 +55,7 @@
      | ClockMeta string
 and
   Case_item
-     = case_item (Expression list) Statement_or_null
+     = case_item "Expression list" Statement_or_null
      | default_case_item Statement_or_null
      | Case_itemMeta string
 and
@@ -112,14 +112,14 @@
 and
   Number
      = decimal string
-     | based (string option) string
+     | based "string option" string
      | NumberMeta string
 and
   Concatenation
-     = concatenation (Expression list) | ConcatenationMeta string
+     = concatenation "Expression list" | ConcatenationMeta string
 and
   Multiple_concatenation
-     = multiple_concatenation Expression (Expression list)
+     = multiple_concatenation Expression "Expression list"
      | Multiple_concatenationMeta string
 and
   meta