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