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.
HEADGOAL;
authorwenzelm
Fri, 28 Jan 2000 21:57:15 +0100
changeset 8168 9d2ac5439089
parent 8167 7574835ed01e
child 8169 77b3bc101de5
HEADGOAL;
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/record_package.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -520,7 +520,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.METHOD0 (HEADGOAL record_split_tac)),
     "split record fields");
 
 
--- a/src/Provers/clasimp.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 28 21:57:15 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 =>
-  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+  HEADGOAL (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 21:56:55 2000 +0100
+++ b/src/Provers/classical.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -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 =>
-  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
+  HEADGOAL (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 21:56:55 2000 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -487,7 +487,7 @@
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
+    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   |> Method.bang_sectioned_args simp_modifiers';
isabelle