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.
replaced FIRSTGOAL by FINDGOAL (backtracking!);
authorwenzelm
Fri, 28 Jan 2000 12:12:06 +0100
changeset 8154 dab09e1ad594
parent 8153 9bdbcb71dc56
child 8155 649c46adfccc
replaced FIRSTGOAL by FINDGOAL (backtracking!);
src/HOL/Tools/induct_method.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions
src/Provers/clasimp.ML file | annotate | diff | comparison | revisions
src/Provers/classical.ML file | annotate | diff | comparison | revisions
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/induct_method.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -72,7 +72,7 @@
 
 fun induct ctxt =
   Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name))
-  >> (fn (is, k) => Method.METHOD (FIRSTGOAL o induct_tac (ProofContext.theory_of ctxt) is k));
+  >> (fn (is, k) => Method.METHOD (FINDGOAL o induct_tac (ProofContext.theory_of ctxt) is k));
 
 fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src);
 val induct_method = ("induct", induct_meth, "induction on types, sets, functions etc.");
--- a/src/HOL/Tools/record_package.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -520,7 +520,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (FIRSTGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)),
     "split record fields");
 
 
--- a/src/Provers/clasimp.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -158,7 +158,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
--- a/src/Provers/classical.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/classical.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -1057,7 +1057,7 @@
 (* METHOD_CLASET' *)
 
 fun METHOD_CLASET' tac ctxt =
-  Method.METHOD (FIRSTGOAL o tac (get_local_claset ctxt));
+  Method.METHOD (FINDGOAL o tac (get_local_claset ctxt));
 
 
 val trace_rules = ref false;
@@ -1149,7 +1149,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
 
 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
+  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
 
 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
--- a/src/Provers/simplifier.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -487,7 +487,7 @@
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
+    FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   |> Method.bang_sectioned_args simp_modifiers';
isabelle