# HG changeset patch # User wenzelm # Date 1507747598 -7200 # Node ID 7ded55dd2a55784e9e18a8599726da96d4f2c265 # Parent 5c32a072ca8bf303be63ccaa999c5843548e75e1 tuned; diff -r 5c32a072ca8b -r 7ded55dd2a55 src/HOL/ROOT --- a/src/HOL/ROOT Wed Oct 11 20:16:00 2017 +0200 +++ b/src/HOL/ROOT Wed Oct 11 20:46:38 2017 +0200 @@ -243,13 +243,13 @@ Generate_Pretty_Char Code_Test_PolyML Code_Test_Scala - theories [condition = "ISABELLE_GHC"] + theories [condition = ISABELLE_GHC] Code_Test_GHC - theories [condition = "ISABELLE_MLTON"] + theories [condition = ISABELLE_MLTON] Code_Test_MLton - theories [condition = "ISABELLE_OCAMLC"] + theories [condition = ISABELLE_OCAMLC] Code_Test_OCaml - theories [condition = "ISABELLE_SMLNJ"] + theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +