equal
deleted
inserted
replaced
1339 |
1339 |
1340 |
1340 |
1341 (** method setup **) |
1341 (** method setup **) |
1342 |
1342 |
1343 fun blast_args m = |
1343 fun blast_args m = |
1344 Method.sectioned_args (Args.bang_facts -- Scan.lift (Scan.option Args.nat)) Data.cla_modifiers m; |
1344 Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; |
1345 |
1345 |
1346 fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems |
1346 fun blast_meth None = Data.cla_meth' blast_tac |
1347 | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems; |
1347 | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim); |
1348 |
1348 |
1349 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]]; |
1349 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]]; |
1350 |
1350 |
1351 |
1351 |
1352 end; |
1352 end; |