equal
deleted
inserted
replaced
101 val [mepo_s, mash_s, mesh_s, isar_s] = |
101 val [mepo_s, mash_s, mesh_s, isar_s] = |
102 [fn () => prove mepo_ok MePoN fst mepo_facts, |
102 [fn () => prove mepo_ok MePoN fst mepo_facts, |
103 fn () => prove mash_ok MaShN fst mash_facts, |
103 fn () => prove mash_ok MaShN fst mash_facts, |
104 fn () => prove mesh_ok MeshN I mesh_facts, |
104 fn () => prove mesh_ok MeshN I mesh_facts, |
105 fn () => prove isar_ok IsarN fst isar_facts] |
105 fn () => prove isar_ok IsarN fst isar_facts] |
106 |> Par_List.map (fn f => f ()) |
106 |> map (fn f => f ()) |
107 in |
107 in |
108 ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, |
108 ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, |
109 isar_s] |
109 isar_s] |
110 |> cat_lines |> print |
110 |> cat_lines |> print |
111 end |
111 end |