375 Generate_Abstract_Char |
375 Generate_Abstract_Char |
376 Generate_Efficient_Datastructures |
376 Generate_Efficient_Datastructures |
377 Code_Lazy_Test |
377 Code_Lazy_Test |
378 Code_Test_PolyML |
378 Code_Test_PolyML |
379 Code_Test_Scala |
379 Code_Test_Scala |
380 theories [condition = "ISABELLE_GHC,ISABELLE_OCAMLFIND"] |
|
381 Generate_Target_String_Literals |
380 Generate_Target_String_Literals |
382 Generate_Target_Bit_Operations |
381 Generate_Target_Bit_Operations |
|
382 theories [condition = ISABELLE_MLTON] |
|
383 Generate_Target_MLton |
|
384 theories [condition = ISABELLE_SMLNJ] |
|
385 Generate_Target_SMLNJ |
|
386 theories [condition = ISABELLE_OCAMLFIND] |
|
387 Generate_Target_OCaml |
|
388 theories [condition = ISABELLE_GHC] |
|
389 Generate_Target_GHC |
|
390 theories [condition = ISABELLE_MLTON] |
|
391 Code_Test_MLton |
|
392 theories [condition = ISABELLE_SMLNJ] |
|
393 Code_Test_SMLNJ |
|
394 theories [condition = ISABELLE_OCAMLFIND] |
|
395 Code_Test_OCaml |
383 theories [condition = ISABELLE_GHC] |
396 theories [condition = ISABELLE_GHC] |
384 Code_Test_GHC |
397 Code_Test_GHC |
385 theories [condition = ISABELLE_MLTON] |
|
386 Code_Test_MLton |
|
387 theories [condition = ISABELLE_OCAMLFIND] |
|
388 Code_Test_OCaml |
|
389 theories [condition = ISABELLE_SMLNJ] |
|
390 Code_Test_SMLNJ |
|
391 |
398 |
392 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + |
399 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + |
393 description " |
400 description " |
394 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
401 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
395 Author: Jasmin Blanchette, TU Muenchen |
402 Author: Jasmin Blanchette, TU Muenchen |