equal
deleted
inserted
replaced
66 swrappers: (string * wrapper) list, |
66 swrappers: (string * wrapper) list, |
67 uwrappers: (string * wrapper) list, |
67 uwrappers: (string * wrapper) list, |
68 safe0_netpair: netpair, safep_netpair: netpair, |
68 safe0_netpair: netpair, safep_netpair: netpair, |
69 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} |
69 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} |
70 val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list |
70 val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list |
71 val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method |
71 val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method |
72 end; |
72 end; |
73 |
73 |
74 |
74 |
75 signature BLAST = |
75 signature BLAST = |
76 sig |
76 sig |
1328 I)); |
1328 I)); |
1329 |
1329 |
1330 |
1330 |
1331 (** method setup **) |
1331 (** method setup **) |
1332 |
1332 |
1333 val blast_args = |
1333 fun blast_args m = |
1334 Method.sectioned_args (K (Scan.lift (Scan.option Args.nat))) Data.cla_modifiers; |
1334 Method.sectioned_args (K (Args.bang_facts -- Scan.lift (Scan.option Args.nat))) Data.cla_modifiers m; |
1335 |
1335 |
1336 fun blast_meth None = Data.cla_meth' blast_tac |
1336 fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems |
1337 | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim); |
1337 | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems; |
1338 |
1338 |
1339 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]]; |
1339 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]]; |
1340 |
1340 |
1341 |
1341 |
1342 end; |
1342 end; |