Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Method.bang_sectioned_args';
authorwenzelm
Fri, 01 Sep 2000 00:36:08 +0200
changeset 9779 c71a1acffc27
parent 9778 1f6dca5c4bbb
child 9780 d25d6a977ea6
Method.bang_sectioned_args';
src/Provers/blast.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/blast.ML	Fri Sep 01 00:34:07 2000 +0200
+++ b/src/Provers/blast.ML	Fri Sep 01 00:36:08 2000 +0200
@@ -1341,10 +1341,10 @@
 (** method setup **)
 
 fun blast_args m =
-  Method.sectioned_args (Args.bang_facts -- Scan.lift (Scan.option Args.nat)) Data.cla_modifiers m;
+  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
 
-fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems
-  | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems;
+fun blast_meth None = Data.cla_meth' blast_tac
+  | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
 
 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
isabelle