src/HOL/ROOT
changeset 58312 710f56e192fe
parent 58309 a09ec6daaa19
child 58313 57d2e5006d29
     1.1 --- a/src/HOL/ROOT	Thu Sep 11 19:35:38 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Sep 11 19:38:22 2014 +0200
     1.3 @@ -732,7 +732,7 @@
     1.4  
     1.5  session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
     1.6    description {*
     1.7 -    (Co)datatype Examples.
     1.8 +    (Co)datatype Examples, including large ones from John Harrison.
     1.9    *}
    1.10    options [document = false]
    1.11    theories
    1.12 @@ -748,7 +748,7 @@
    1.13      Misc_Datatype
    1.14      Misc_Primcorec
    1.15      Misc_Primrec
    1.16 -  theories [condition = ISABELLE_FULL_TEST]
    1.17 +  theories [condition = ISABELLE_FULL_TEST, timing]
    1.18      Brackin
    1.19      Instructions
    1.20      IsaFoR_Datatypes
    1.21 @@ -1085,17 +1085,6 @@
    1.22      TrivEx
    1.23      TrivEx2
    1.24  
    1.25 -session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
    1.26 -  description {*
    1.27 -    Some rather large datatype examples (from John Harrison).
    1.28 -  *}
    1.29 -  options [document = false]
    1.30 -  theories [condition = ISABELLE_FULL_TEST, timing]
    1.31 -    Brackin
    1.32 -    Instructions
    1.33 -    SML
    1.34 -    Verilog
    1.35 -
    1.36  session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
    1.37    description {*
    1.38      Some benchmark on large record.