src/Benchmarks/Datatype_Benchmark/IsaFoR.thy
changeset 66453 cc19f7ca2ed6
parent 62290 658276428cfc
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     6 *)
     6 *)
     7 
     7 
     8 section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close>
     8 section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close>
     9 
     9 
    10 theory IsaFoR
    10 theory IsaFoR
    11 imports Real
    11 imports HOL.Real
    12 begin
    12 begin
    13 
    13 
    14 datatype (discs_sels) ('f, 'l) lab =
    14 datatype (discs_sels) ('f, 'l) lab =
    15     Lab "('f, 'l) lab" 'l
    15     Lab "('f, 'l) lab" 'l
    16   | FunLab "('f, 'l) lab" "('f, 'l) lab list"
    16   | FunLab "('f, 'l) lab" "('f, 'l) lab list"