59 val ccontr : thm |
59 val ccontr : thm |
60 val contr_tac : int -> tactic |
60 val contr_tac : int -> tactic |
61 val dup_intr : thm -> thm |
61 val dup_intr : thm -> thm |
62 val hyp_subst_tac : bool ref -> int -> tactic |
62 val hyp_subst_tac : bool ref -> int -> tactic |
63 val claset : unit -> claset |
63 val claset : unit -> claset |
64 val rep_claset : (* dependent on classical.ML *) |
64 val rep_cs : (* dependent on classical.ML *) |
65 claset -> {safeIs: thm list, safeEs: thm list, |
65 claset -> {safeIs: thm list, safeEs: thm list, |
66 hazIs: thm list, hazEs: thm list, |
66 hazIs: thm list, hazEs: thm list, |
67 swrappers: (string * wrapper) list, |
67 swrappers: (string * wrapper) list, |
68 uwrappers: (string * wrapper) list, |
68 uwrappers: (string * wrapper) list, |
69 safe0_netpair: netpair, safep_netpair: netpair, |
69 safe0_netpair: netpair, safep_netpair: netpair, |
916 branch contains a list of unexpanded formulae, a list of literals, and a |
916 branch contains a list of unexpanded formulae, a list of literals, and a |
917 bound on unsafe expansions. |
917 bound on unsafe expansions. |
918 "start" is CPU time at start, for printing search time |
918 "start" is CPU time at start, for printing search time |
919 *) |
919 *) |
920 fun prove (sign, start, cs, brs, cont) = |
920 fun prove (sign, start, cs, brs, cont) = |
921 let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs |
921 let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs |
922 val safeList = [safe0_netpair, safep_netpair] |
922 val safeList = [safe0_netpair, safep_netpair] |
923 and hazList = [haz_netpair] |
923 and hazList = [haz_netpair] |
924 fun prv (tacs, trs, choices, []) = |
924 fun prv (tacs, trs, choices, []) = |
925 (printStats (!trace orelse !stats, start, tacs); |
925 (printStats (!trace orelse !stats, start, tacs); |
926 cont (tacs, trs, choices)) (*all branches closed!*) |
926 cont (tacs, trs, choices)) (*all branches closed!*) |