equal
deleted
inserted
replaced
55 swrappers: (string * wrapper) list, |
55 swrappers: (string * wrapper) list, |
56 uwrappers: (string * wrapper) list, |
56 uwrappers: (string * wrapper) list, |
57 safe0_netpair: netpair, safep_netpair: netpair, |
57 safe0_netpair: netpair, safep_netpair: netpair, |
58 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair} |
58 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair} |
59 val cla_modifiers: Method.modifier parser list |
59 val cla_modifiers: Method.modifier parser list |
60 val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method |
60 val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method |
61 end; |
61 end; |
62 |
62 |
63 signature BLAST = |
63 signature BLAST = |
64 sig |
64 sig |
65 type claset |
65 type claset |
1307 (** method setup **) |
1307 (** method setup **) |
1308 |
1308 |
1309 val setup = |
1309 val setup = |
1310 setup_depth_limit #> |
1310 setup_depth_limit #> |
1311 Method.setup @{binding blast} |
1311 Method.setup @{binding blast} |
1312 (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --| |
1312 (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >> |
1313 Method.sections Data.cla_modifiers >> |
1313 (fn NONE => Data.cla_meth' blast_tac |
1314 (fn (prems, NONE) => Data.cla_meth' blast_tac prems |
1314 | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim))) |
1315 | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems)) |
|
1316 "classical tableau prover"; |
1315 "classical tableau prover"; |
1317 |
1316 |
1318 end; |
1317 end; |