equal
deleted
inserted
replaced
235 Generate |
235 Generate |
236 Generate_Binary_Nat |
236 Generate_Binary_Nat |
237 Generate_Target_Nat |
237 Generate_Target_Nat |
238 Generate_Efficient_Datastructures |
238 Generate_Efficient_Datastructures |
239 Generate_Pretty_Char |
239 Generate_Pretty_Char |
|
240 Code_Test |
|
241 theories[condition = ISABELLE_GHC] |
|
242 Code_Test_GHC |
|
243 theories[condition = ISABELLE_MLTON] |
|
244 Code_Test_MLton |
|
245 theories[condition = ISABELLE_OCAMLC] |
|
246 Code_Test_OCaml |
|
247 theories[condition = ISABELLE_POLYML_PATH] |
|
248 Code_Test_PolyML |
|
249 theories[condition = ISABELLE_SCALA] |
|
250 Code_Test_Scala |
|
251 theories[condition = ISABELLE_SMLNJ] |
|
252 Code_Test_SMLNJ |
240 |
253 |
241 session "HOL-Metis_Examples" in Metis_Examples = HOL + |
254 session "HOL-Metis_Examples" in Metis_Examples = HOL + |
242 description {* |
255 description {* |
243 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
256 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
244 Author: Jasmin Blanchette, TU Muenchen |
257 Author: Jasmin Blanchette, TU Muenchen |