diff -r f8e6197668c9 -r 469a375212c1 src/HOL/ROOT --- a/src/HOL/ROOT Mon Aug 25 09:08:45 2014 +0200 +++ b/src/HOL/ROOT Mon Aug 25 09:40:50 2014 +0200 @@ -237,6 +237,19 @@ Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char + Code_Test + theories[condition = ISABELLE_GHC] + Code_Test_GHC + theories[condition = ISABELLE_MLTON] + Code_Test_MLton + theories[condition = ISABELLE_OCAMLC] + Code_Test_OCaml + theories[condition = ISABELLE_POLYML_PATH] + Code_Test_PolyML + theories[condition = ISABELLE_SCALA] + Code_Test_Scala + theories[condition = ISABELLE_SMLNJ] + Code_Test_SMLNJ session "HOL-Metis_Examples" in Metis_Examples = HOL + description {*