doc-src/Codegen/Thy/Setup.thy
changeset 39066 4517a4049588
parent 38798 89f273ab1d42
child 42288 2074b31650e6
equal deleted inserted replaced
39065:16a2ed09217a 39066:4517a4049588
     1 theory Setup
     1 theory Setup
     2 imports Complex_Main More_List RBT Dlist Mapping
     2 imports
       
     3   Complex_Main
       
     4   More_List RBT Dlist Mapping
     3 uses
     5 uses
     4   "../../antiquote_setup.ML"
     6   "../../antiquote_setup.ML"
     5   "../../more_antiquote.ML"
     7   "../../more_antiquote.ML"
     6 begin
     8 begin
     7 
       
     8 ML {* no_document use_thys
       
     9   ["Efficient_Nat", "Code_Char_chr", "Product_ord",
       
    10    "~~/src/HOL/Imperative_HOL/Imperative_HOL",
       
    11    "~~/src/HOL/Decision_Procs/Ferrack"] *}
       
    12 
     9 
    13 setup {*
    10 setup {*
    14 let
    11 let
    15   val typ = Simple_Syntax.read_typ;
    12   val typ = Simple_Syntax.read_typ;
    16   val typeT = Syntax.typeT;
    13   val typeT = Syntax.typeT;