Admin/Benchmarks/HOL-datatype/Verilog.thy
changeset 33695 bec342db1bf4
parent 22875 9b21fa38a3cf
equal deleted inserted replaced
33694:f06fe9c2152d 33695:bec342db1bf4
     1 (*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
     1 (*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
     2     ID:         $Id$
     2 
       
     3 Example from Daryl: a Verilog grammar.
     3 *)
     4 *)
     4 
     5 
     5 theory Verilog imports Main begin
     6 theory Verilog imports Main begin
     6 
       
     7 (* ------------------------------------------------------------------------- *)
       
     8 (* Example from Daryl: a Verilog grammar.                                    *)
       
     9 (* ------------------------------------------------------------------------- *)
       
    10 
     7 
    11 datatype
     8 datatype
    12   Source_text
     9   Source_text
    13      = module string "string list" "Module_item list"
    10      = module string "string list" "Module_item list"
    14      | Source_textMeta string
    11      | Source_textMeta string