equal
deleted
inserted
replaced
4 |
4 |
5 structure Mirabelle_Refute : MIRABELLE_ACTION = |
5 structure Mirabelle_Refute : MIRABELLE_ACTION = |
6 struct |
6 struct |
7 |
7 |
8 |
8 |
|
9 (* FIXME: |
9 fun refute_action args {pre=st, ...} = |
10 fun refute_action args {pre=st, ...} = |
10 let |
11 let |
11 val subgoal = 0 |
12 val subgoal = 0 |
12 val thy = Proof.theory_of st |
13 val thy = Proof.theory_of st |
13 val thm = goal_thm_of st |
14 val thm = goal_thm_of st |
28 then SOME "no counterexample (time out)" |
29 then SOME "no counterexample (time out)" |
29 else if Substring.isSubstring "Search terminated" writ_log |
30 else if Substring.isSubstring "Search terminated" writ_log |
30 then SOME "no counterexample (normal termination)" |
31 then SOME "no counterexample (normal termination)" |
31 else SOME "no counterexample (unknown)" |
32 else SOME "no counterexample (unknown)" |
32 in r end |
33 in r end |
|
34 *) |
33 |
35 |
34 fun invoke args = Mirabelle.register ("refute", refute_action args) |
36 fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) |
35 |
37 |
36 end |
38 end |