# HG changeset patch
# User blanchet
# Date 1410456023 -7200
# Node ID 0ccba1b6d00bc7a400e94ce14bece672085f91bd
# Parent  8172bbb37b0622de69102889bc5235f06b21ef7d
move datatype benchmarks

diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/BNF_Examples/Brackin.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Brackin.thy	Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Datatype_Benchmark/Brackin.thy
+
+A couple of datatypes from Steve Brackin's work.
+*)
+
+theory Brackin imports Main begin
+
+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 |
+    X32 | X33 | X34
+
+datatype ('a, 'b, 'c) TY1 =
+      NoF
+    | Fk 'a "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY2 =
+      Ta bool
+    | Td bool
+    | 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"
+and ('a, 'b, 'c) TY3 =
+      NoS
+    | 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"
+
+end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/BNF_Examples/Instructions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Instructions.thy	Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,162 @@
+(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
+
+Example from Konrad: 68000 instruction set.
+*)
+
+theory Instructions imports Main begin
+
+datatype Size = Byte | Word | Long
+
+datatype DataRegister =
+  RegD0
+| RegD1
+| RegD2
+| RegD3
+| RegD4
+| RegD5
+| RegD6
+| RegD7
+
+datatype AddressRegister =
+  RegA0
+| RegA1
+| RegA2
+| RegA3
+| RegA4
+| RegA5
+| RegA6
+| RegA7
+
+datatype DataOrAddressRegister =
+  data DataRegister
+| address AddressRegister
+
+datatype Condition =
+  Hi
+| Ls
+| Cc
+| Cs
+| Ne
+| Eq
+| Vc
+| Vs
+| Pl
+| Mi
+| Ge
+| Lt
+| Gt
+| Le
+
+datatype AddressingMode =
+  immediate nat
+| direct DataOrAddressRegister
+| indirect AddressRegister
+| postinc AddressRegister
+| predec AddressRegister
+| indirectdisp nat AddressRegister
+| indirectindex nat AddressRegister DataOrAddressRegister Size
+| absolute nat
+| pcdisp nat
+| pcindex nat DataOrAddressRegister Size
+
+datatype M68kInstruction =
+  ABCD AddressingMode AddressingMode
+| ADD Size AddressingMode AddressingMode
+| ADDA Size AddressingMode AddressRegister
+| ADDI Size nat AddressingMode
+| ADDQ Size nat AddressingMode
+| ADDX Size AddressingMode AddressingMode
+| AND Size AddressingMode AddressingMode
+| ANDI Size nat AddressingMode
+| ANDItoCCR nat
+| ANDItoSR nat
+| ASL Size AddressingMode DataRegister
+| ASLW AddressingMode
+| ASR Size AddressingMode DataRegister
+| ASRW AddressingMode
+| Bcc Condition Size nat
+| BTST Size AddressingMode AddressingMode
+| BCHG Size AddressingMode AddressingMode
+| BCLR Size AddressingMode AddressingMode
+| BSET Size AddressingMode AddressingMode
+| BRA Size nat
+| BSR Size nat
+| CHK AddressingMode DataRegister
+| CLR Size AddressingMode
+| CMP Size AddressingMode DataRegister
+| CMPA Size AddressingMode AddressRegister
+| CMPI Size nat AddressingMode
+| CMPM Size AddressRegister AddressRegister
+| DBT DataRegister nat
+| DBF DataRegister nat
+| DBcc Condition DataRegister nat
+| DIVS AddressingMode DataRegister
+| DIVU AddressingMode DataRegister
+| EOR Size DataRegister AddressingMode
+| EORI Size nat AddressingMode
+| EORItoCCR nat
+| EORItoSR nat
+| EXG DataOrAddressRegister DataOrAddressRegister
+| EXT Size DataRegister
+| ILLEGAL
+| JMP AddressingMode
+| JSR AddressingMode
+| LEA AddressingMode AddressRegister
+| LINK AddressRegister nat
+| LSL Size AddressingMode DataRegister
+| LSLW AddressingMode
+| LSR Size AddressingMode DataRegister
+| LSRW AddressingMode
+| MOVE Size AddressingMode AddressingMode
+| MOVEtoCCR AddressingMode
+| MOVEtoSR AddressingMode
+| MOVEfromSR AddressingMode
+| MOVEtoUSP AddressingMode
+| MOVEfromUSP AddressingMode
+| MOVEA Size AddressingMode AddressRegister
+| MOVEMto Size AddressingMode "DataOrAddressRegister list"
+| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
+| MOVEP Size AddressingMode AddressingMode
+| MOVEQ nat DataRegister
+| MULS AddressingMode DataRegister
+| MULU AddressingMode DataRegister
+| NBCD AddressingMode
+| NEG Size AddressingMode
+| NEGX Size AddressingMode
+| NOP
+| NOT Size AddressingMode
+| OR Size AddressingMode AddressingMode
+| ORI Size nat AddressingMode
+| ORItoCCR nat
+| ORItoSR nat
+| PEA AddressingMode
+| RESET
+| ROL Size AddressingMode DataRegister
+| ROLW AddressingMode
+| ROR Size AddressingMode DataRegister
+| RORW AddressingMode
+| ROXL Size AddressingMode DataRegister
+| ROXLW AddressingMode
+| ROXR Size AddressingMode DataRegister
+| ROXRW AddressingMode
+| RTE
+| RTR
+| RTS
+| SBCD AddressingMode AddressingMode
+| ST AddressingMode
+| SF AddressingMode
+| Scc Condition AddressingMode
+| STOP nat
+| SUB Size AddressingMode AddressingMode
+| SUBA Size AddressingMode AddressingMode
+| SUBI Size nat AddressingMode
+| SUBQ Size nat AddressingMode
+| SUBX Size AddressingMode AddressingMode
+| SWAP DataRegister
+| TAS AddressingMode
+| TRAP nat
+| TRAPV
+| TST Size AddressingMode
+| UNLK AddressRegister
+
+end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/BNF_Examples/SML.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/SML.thy	Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,91 @@
+(*  Title:      HOL/Datatype_Benchmark/SML.thy
+
+Example from Myra: part of the syntax of SML.
+*)
+
+theory SML imports Main begin
+
+datatype
+  string = EMPTY_STRING | CONS_STRING nat string
+
+datatype
+   strid = STRID string
+
+datatype
+   var = VAR string
+
+datatype
+   con = CON string
+
+datatype
+   scon = SCINT nat | SCSTR string
+
+datatype
+   excon = EXCON string
+
+datatype
+   label = LABEL string
+
+datatype
+  'a nonemptylist = Head_and_tail 'a "'a list"
+
+datatype
+  '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"
+           | PARatpat_e pat_e
+and
+   patrow_e = DOTDOTDOT_e
+            | 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
+         | LAYEREDpat_e var pat_e
+and
+   conbind_e = CONBIND_e con "conbind_e option"
+and
+   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"
+and
+   atexp_e = SCONatexp_e scon
+           | 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"
+and
+   exp_e = ATEXPexp_e atexp_e
+         | APPexp_e exp_e atexp_e
+         | HANDLEexp_e exp_e match_e
+         | RAISEexp_e exp_e
+         | FNexp_e match_e
+and
+   match_e = MATCH_e mrule_e "match_e option"
+and
+   mrule_e = MRULE_e pat_e exp_e
+and
+   dec_e = VALdec_e valbind_e
+         | DATATYPEdec_e datbind_e
+         | ABSTYPEdec_e datbind_e dec_e
+         | EXCEPTdec_e exbind_e
+         | LOCALdec_e dec_e dec_e
+         | 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"
+             | RECvalbind_e valbind_e
+
+end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/BNF_Examples/Verilog.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/Verilog.thy	Thu Sep 11 19:20:23 2014 +0200
@@ -0,0 +1,138 @@
+(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
+
+Example from Daryl: a Verilog grammar.
+*)
+
+theory Verilog imports Main begin
+
+datatype
+  Source_text
+     = module string "string list" "Module_item list"
+     | Source_textMeta string
+and
+  Module_item
+     = "declaration" Declaration
+     | initial Statement
+     | always Statement
+     | assign Lvalue Expression
+     | 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"
+     | DeclarationMeta string
+and
+  Range = range Expression Expression | RangeMeta string
+and
+  Statement
+     = clock_statement Clock Statement_or_null
+     | 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"
+     | 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"
+     | StatementMeta string
+and
+  Statement_or_null
+     = statement Statement | null_statement | Statement_or_nullMeta string
+and
+  Clock
+     = posedge string
+     | negedge string
+     | clock string
+     | ClockMeta string
+and
+  Case_item
+     = case_item "Expression list" Statement_or_null
+     | default_case_item Statement_or_null
+     | Case_itemMeta string
+and
+  Expression
+     = plus Expression Expression
+     | minus Expression Expression
+     | lshift Expression Expression
+     | rshift Expression Expression
+     | lt Expression Expression
+     | leq Expression Expression
+     | gt Expression Expression
+     | geq Expression Expression
+     | logeq Expression Expression
+     | logneq Expression Expression
+     | caseeq Expression Expression
+     | caseneq Expression Expression
+     | bitand Expression Expression
+     | bitxor Expression Expression
+     | bitor Expression Expression
+     | logand Expression Expression
+     | logor Expression Expression
+     | conditional Expression Expression Expression
+     | positive Primary
+     | negative Primary
+     | lognot Primary
+     | bitnot Primary
+     | reducand Primary
+     | reducxor Primary
+     | reducor Primary
+     | reducnand Primary
+     | reducxnor Primary
+     | reducnor Primary
+     | primary Primary
+     | ExpressionMeta string
+and
+  Primary
+     = primary_number Number
+     | primary_IDENTIFIER string
+     | primary_bit_select string Expression
+     | primary_part_select string Expression Expression
+     | primary_gen_bit_select Expression Expression
+     | primary_gen_part_select Expression Expression Expression
+     | primary_concatenation Concatenation
+     | primary_multiple_concatenation Multiple_concatenation
+     | brackets Expression
+     | PrimaryMeta string
+and
+  Lvalue
+     = lvalue string
+     | lvalue_bit_select string Expression
+     | lvalue_part_select string Expression Expression
+     | lvalue_concatenation Concatenation
+     | LvalueMeta string
+and
+  Number
+     = decimal string
+     | based "string option" string
+     | NumberMeta string
+and
+  Concatenation
+     = concatenation "Expression list" | ConcatenationMeta string
+and
+  Multiple_concatenation
+     = multiple_concatenation Expression "Expression list"
+     | Multiple_concatenationMeta string
+and
+  meta
+     = Meta_Source_text Source_text
+     | Meta_Module_item Module_item
+     | Meta_Declaration Declaration
+     | Meta_Range Range
+     | Meta_Statement Statement
+     | Meta_Statement_or_null Statement_or_null
+     | Meta_Clock Clock
+     | Meta_Case_item Case_item
+     | Meta_Expression Expression
+     | Meta_Primary Primary
+     | Meta_Lvalue Lvalue
+     | Meta_Number Number
+     | Meta_Concatenation Concatenation
+     | Meta_Multiple_concatenation Multiple_concatenation
+
+end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/Datatype_Benchmark/Brackin.thy
--- a/src/HOL/Datatype_Benchmark/Brackin.thy	Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/Datatype_Benchmark/Brackin.thy
-
-A couple of datatypes from Steve Brackin's work.
-*)
-
-theory Brackin imports Main begin
-
-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 |
-    X32 | X33 | X34
-
-datatype ('a, 'b, 'c) TY1 =
-      NoF
-    | Fk 'a "('a, 'b, 'c) TY2"
-and ('a, 'b, 'c) TY2 =
-      Ta bool
-    | Td bool
-    | 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"
-and ('a, 'b, 'c) TY3 =
-      NoS
-    | 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"
-
-end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/Datatype_Benchmark/Instructions.thy
--- a/src/HOL/Datatype_Benchmark/Instructions.thy	Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
-
-Example from Konrad: 68000 instruction set.
-*)
-
-theory Instructions imports Main begin
-
-datatype Size = Byte | Word | Long
-
-datatype DataRegister =
-  RegD0
-| RegD1
-| RegD2
-| RegD3
-| RegD4
-| RegD5
-| RegD6
-| RegD7
-
-datatype AddressRegister =
-  RegA0
-| RegA1
-| RegA2
-| RegA3
-| RegA4
-| RegA5
-| RegA6
-| RegA7
-
-datatype DataOrAddressRegister =
-  data DataRegister
-| address AddressRegister
-
-datatype Condition =
-  Hi
-| Ls
-| Cc
-| Cs
-| Ne
-| Eq
-| Vc
-| Vs
-| Pl
-| Mi
-| Ge
-| Lt
-| Gt
-| Le
-
-datatype AddressingMode =
-  immediate nat
-| direct DataOrAddressRegister
-| indirect AddressRegister
-| postinc AddressRegister
-| predec AddressRegister
-| indirectdisp nat AddressRegister
-| indirectindex nat AddressRegister DataOrAddressRegister Size
-| absolute nat
-| pcdisp nat
-| pcindex nat DataOrAddressRegister Size
-
-datatype M68kInstruction =
-  ABCD AddressingMode AddressingMode
-| ADD Size AddressingMode AddressingMode
-| ADDA Size AddressingMode AddressRegister
-| ADDI Size nat AddressingMode
-| ADDQ Size nat AddressingMode
-| ADDX Size AddressingMode AddressingMode
-| AND Size AddressingMode AddressingMode
-| ANDI Size nat AddressingMode
-| ANDItoCCR nat
-| ANDItoSR nat
-| ASL Size AddressingMode DataRegister
-| ASLW AddressingMode
-| ASR Size AddressingMode DataRegister
-| ASRW AddressingMode
-| Bcc Condition Size nat
-| BTST Size AddressingMode AddressingMode
-| BCHG Size AddressingMode AddressingMode
-| BCLR Size AddressingMode AddressingMode
-| BSET Size AddressingMode AddressingMode
-| BRA Size nat
-| BSR Size nat
-| CHK AddressingMode DataRegister
-| CLR Size AddressingMode
-| CMP Size AddressingMode DataRegister
-| CMPA Size AddressingMode AddressRegister
-| CMPI Size nat AddressingMode
-| CMPM Size AddressRegister AddressRegister
-| DBT DataRegister nat
-| DBF DataRegister nat
-| DBcc Condition DataRegister nat
-| DIVS AddressingMode DataRegister
-| DIVU AddressingMode DataRegister
-| EOR Size DataRegister AddressingMode
-| EORI Size nat AddressingMode
-| EORItoCCR nat
-| EORItoSR nat
-| EXG DataOrAddressRegister DataOrAddressRegister
-| EXT Size DataRegister
-| ILLEGAL
-| JMP AddressingMode
-| JSR AddressingMode
-| LEA AddressingMode AddressRegister
-| LINK AddressRegister nat
-| LSL Size AddressingMode DataRegister
-| LSLW AddressingMode
-| LSR Size AddressingMode DataRegister
-| LSRW AddressingMode
-| MOVE Size AddressingMode AddressingMode
-| MOVEtoCCR AddressingMode
-| MOVEtoSR AddressingMode
-| MOVEfromSR AddressingMode
-| MOVEtoUSP AddressingMode
-| MOVEfromUSP AddressingMode
-| MOVEA Size AddressingMode AddressRegister
-| MOVEMto Size AddressingMode "DataOrAddressRegister list"
-| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
-| MOVEP Size AddressingMode AddressingMode
-| MOVEQ nat DataRegister
-| MULS AddressingMode DataRegister
-| MULU AddressingMode DataRegister
-| NBCD AddressingMode
-| NEG Size AddressingMode
-| NEGX Size AddressingMode
-| NOP
-| NOT Size AddressingMode
-| OR Size AddressingMode AddressingMode
-| ORI Size nat AddressingMode
-| ORItoCCR nat
-| ORItoSR nat
-| PEA AddressingMode
-| RESET
-| ROL Size AddressingMode DataRegister
-| ROLW AddressingMode
-| ROR Size AddressingMode DataRegister
-| RORW AddressingMode
-| ROXL Size AddressingMode DataRegister
-| ROXLW AddressingMode
-| ROXR Size AddressingMode DataRegister
-| ROXRW AddressingMode
-| RTE
-| RTR
-| RTS
-| SBCD AddressingMode AddressingMode
-| ST AddressingMode
-| SF AddressingMode
-| Scc Condition AddressingMode
-| STOP nat
-| SUB Size AddressingMode AddressingMode
-| SUBA Size AddressingMode AddressingMode
-| SUBI Size nat AddressingMode
-| SUBQ Size nat AddressingMode
-| SUBX Size AddressingMode AddressingMode
-| SWAP DataRegister
-| TAS AddressingMode
-| TRAP nat
-| TRAPV
-| TST Size AddressingMode
-| UNLK AddressRegister
-
-end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/Datatype_Benchmark/SML.thy
--- a/src/HOL/Datatype_Benchmark/SML.thy	Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(*  Title:      HOL/Datatype_Benchmark/SML.thy
-
-Example from Myra: part of the syntax of SML.
-*)
-
-theory SML imports Main begin
-
-datatype
-  string = EMPTY_STRING | CONS_STRING nat string
-
-datatype
-   strid = STRID string
-
-datatype
-   var = VAR string
-
-datatype
-   con = CON string
-
-datatype
-   scon = SCINT nat | SCSTR string
-
-datatype
-   excon = EXCON string
-
-datatype
-   label = LABEL string
-
-datatype
-  'a nonemptylist = Head_and_tail 'a "'a list"
-
-datatype
-  '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"
-           | PARatpat_e pat_e
-and
-   patrow_e = DOTDOTDOT_e
-            | 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
-         | LAYEREDpat_e var pat_e
-and
-   conbind_e = CONBIND_e con "conbind_e option"
-and
-   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"
-and
-   atexp_e = SCONatexp_e scon
-           | 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"
-and
-   exp_e = ATEXPexp_e atexp_e
-         | APPexp_e exp_e atexp_e
-         | HANDLEexp_e exp_e match_e
-         | RAISEexp_e exp_e
-         | FNexp_e match_e
-and
-   match_e = MATCH_e mrule_e "match_e option"
-and
-   mrule_e = MRULE_e pat_e exp_e
-and
-   dec_e = VALdec_e valbind_e
-         | DATATYPEdec_e datbind_e
-         | ABSTYPEdec_e datbind_e dec_e
-         | EXCEPTdec_e exbind_e
-         | LOCALdec_e dec_e dec_e
-         | 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"
-             | RECvalbind_e valbind_e
-
-end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/Datatype_Benchmark/Verilog.thy
--- a/src/HOL/Datatype_Benchmark/Verilog.thy	Thu Sep 11 19:18:23 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
-
-Example from Daryl: a Verilog grammar.
-*)
-
-theory Verilog imports Main begin
-
-datatype
-  Source_text
-     = module string "string list" "Module_item list"
-     | Source_textMeta string
-and
-  Module_item
-     = "declaration" Declaration
-     | initial Statement
-     | always Statement
-     | assign Lvalue Expression
-     | 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"
-     | DeclarationMeta string
-and
-  Range = range Expression Expression | RangeMeta string
-and
-  Statement
-     = clock_statement Clock Statement_or_null
-     | 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"
-     | 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"
-     | StatementMeta string
-and
-  Statement_or_null
-     = statement Statement | null_statement | Statement_or_nullMeta string
-and
-  Clock
-     = posedge string
-     | negedge string
-     | clock string
-     | ClockMeta string
-and
-  Case_item
-     = case_item "Expression list" Statement_or_null
-     | default_case_item Statement_or_null
-     | Case_itemMeta string
-and
-  Expression
-     = plus Expression Expression
-     | minus Expression Expression
-     | lshift Expression Expression
-     | rshift Expression Expression
-     | lt Expression Expression
-     | leq Expression Expression
-     | gt Expression Expression
-     | geq Expression Expression
-     | logeq Expression Expression
-     | logneq Expression Expression
-     | caseeq Expression Expression
-     | caseneq Expression Expression
-     | bitand Expression Expression
-     | bitxor Expression Expression
-     | bitor Expression Expression
-     | logand Expression Expression
-     | logor Expression Expression
-     | conditional Expression Expression Expression
-     | positive Primary
-     | negative Primary
-     | lognot Primary
-     | bitnot Primary
-     | reducand Primary
-     | reducxor Primary
-     | reducor Primary
-     | reducnand Primary
-     | reducxnor Primary
-     | reducnor Primary
-     | primary Primary
-     | ExpressionMeta string
-and
-  Primary
-     = primary_number Number
-     | primary_IDENTIFIER string
-     | primary_bit_select string Expression
-     | primary_part_select string Expression Expression
-     | primary_gen_bit_select Expression Expression
-     | primary_gen_part_select Expression Expression Expression
-     | primary_concatenation Concatenation
-     | primary_multiple_concatenation Multiple_concatenation
-     | brackets Expression
-     | PrimaryMeta string
-and
-  Lvalue
-     = lvalue string
-     | lvalue_bit_select string Expression
-     | lvalue_part_select string Expression Expression
-     | lvalue_concatenation Concatenation
-     | LvalueMeta string
-and
-  Number
-     = decimal string
-     | based "string option" string
-     | NumberMeta string
-and
-  Concatenation
-     = concatenation "Expression list" | ConcatenationMeta string
-and
-  Multiple_concatenation
-     = multiple_concatenation Expression "Expression list"
-     | Multiple_concatenationMeta string
-and
-  meta
-     = Meta_Source_text Source_text
-     | Meta_Module_item Module_item
-     | Meta_Declaration Declaration
-     | Meta_Range Range
-     | Meta_Statement Statement
-     | Meta_Statement_or_null Statement_or_null
-     | Meta_Clock Clock
-     | Meta_Case_item Case_item
-     | Meta_Expression Expression
-     | Meta_Primary Primary
-     | Meta_Lvalue Lvalue
-     | Meta_Number Number
-     | Meta_Concatenation Concatenation
-     | Meta_Multiple_concatenation Multiple_concatenation
-
-end
diff -r 8172bbb37b06 -r 0ccba1b6d00b src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 11 19:18:23 2014 +0200
+++ b/src/HOL/ROOT	Thu Sep 11 19:20:23 2014 +0200
@@ -749,7 +749,11 @@
     Misc_Primcorec
     Misc_Primrec
   theories [condition = ISABELLE_FULL_TEST]
+    Brackin
+    Instructions
     IsaFoR_Datatypes
+    SML
+    Verilog
 
 session "HOL-Word" (main) in Word = HOL +
   options [document_graph]