src/HOL/ROOT
changeset 58415 8392d221bd91
parent 58413 22dd971f6938
child 58418 a04b242a7a01
     1.1 --- a/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Mon Sep 22 10:18:41 2014 +0200
     1.3 @@ -242,17 +242,17 @@
     1.4      Generate_Efficient_Datastructures
     1.5      Generate_Pretty_Char
     1.6      Code_Test
     1.7 -  theories[condition = ISABELLE_GHC]
     1.8 +  theories [condition = ISABELLE_GHC]
     1.9      Code_Test_GHC
    1.10 -  theories[condition = ISABELLE_MLTON]
    1.11 +  theories [condition = ISABELLE_MLTON]
    1.12      Code_Test_MLton
    1.13 -  theories[condition = ISABELLE_OCAMLC]
    1.14 +  theories [condition = ISABELLE_OCAMLC]
    1.15      Code_Test_OCaml
    1.16 -  theories[condition = ISABELLE_POLYML_PATH]
    1.17 +  theories [condition = ISABELLE_POLYML]
    1.18      Code_Test_PolyML
    1.19 -  theories[condition = ISABELLE_SCALA]
    1.20 +  theories [condition = ISABELLE_SCALA]
    1.21      Code_Test_Scala
    1.22 -  theories[condition = ISABELLE_SMLNJ]
    1.23 +  theories [condition = ISABELLE_SMLNJ]
    1.24      Code_Test_SMLNJ
    1.25  
    1.26  session "HOL-Metis_Examples" in Metis_Examples = HOL +