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.
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
authorwenzelm
Sat, 18 Nov 2000 19:47:36 +0100
changeset 10493 76e05ec87b57
parent 10492 107c7db021a9
child 10494 305b37c8d8a3
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Sat Nov 18 19:47:12 2000 +0100
+++ b/src/Pure/axclass.ML	Sat Nov 18 19:47:36 2000 +0100
@@ -318,8 +318,9 @@
 
 (* default method *)
 
-fun default_intro_classes_tac [] = intro_classes_tac []
-  | default_intro_classes_tac _ = K Tactical.no_tac;    (*no error message!*)
+fun default_intro_classes_tac [] i = intro_classes_tac [] i THEN
+      Tactic.distinct_subgoals_tac    (*affects all subgoals, which is usually OK*)
+  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
 
 fun default_tac rules ctxt facts =
   HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
isabelle