equal
deleted
inserted
replaced
1852 in TPTP_Reconstruction_Data.map (cons ((prob_name, pannot))) thy5 end |
1852 in TPTP_Reconstruction_Data.map (cons ((prob_name, pannot))) thy5 end |
1853 end |
1853 end |
1854 |
1854 |
1855 (*This has been disabled since it requires a hook to be specified to use "import_thm" |
1855 (*This has been disabled since it requires a hook to be specified to use "import_thm" |
1856 val _ = |
1856 val _ = |
1857 Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof" |
1857 Outer_Syntax.command @{command_keyword import_leo2_proof} "import TPTP proof" |
1858 (Parse.path >> (fn name => |
1858 (Parse.path >> (fn name => |
1859 Toplevel.theory (fn thy => |
1859 Toplevel.theory (fn thy => |
1860 let val path = Path.explode name |
1860 let val path = Path.explode name |
1861 in import_thm true [Path.dir path, Path.explode "$TPTP"] path (*FIXME hook needs to be given here*) |
1861 in import_thm true [Path.dir path, Path.explode "$TPTP"] path (*FIXME hook needs to be given here*) |
1862 thy end))) |
1862 thy end))) |