equal
deleted
inserted
replaced
7 |
7 |
8 |
8 |
9 (* FIXME: |
9 (* FIXME: |
10 fun refute_action args timeout {pre=st, ...} = |
10 fun refute_action args timeout {pre=st, ...} = |
11 let |
11 let |
12 val subgoal = 0 |
12 val subgoal = 1 |
13 val thy = Proof.theory_of st |
13 val thy = Proof.theory_of st |
14 val thm = goal_thm_of st |
14 val thm = goal_thm_of st |
15 |
15 |
16 val refute = Refute.refute_subgoal thy args thm |
16 val refute = Refute.refute_goal thy args thm |
17 val _ = TimeLimit.timeLimit timeout refute subgoal |
17 val _ = TimeLimit.timeLimit timeout refute subgoal |
18 in |
18 in |
19 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
19 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
20 val warn_log = Substring.full (the (Symtab.lookup tab "warning")) |
20 val warn_log = Substring.full (the (Symtab.lookup tab "warning")) |
21 |
21 |