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.
Changed to use split instead of fsplit. The weakening of fsplitE appears not
authorlcp
Wed, 03 May 1995 17:30:36 +0200
changeset 1104 141f73abbafc
parent 1103 08fda5148971
child 1105 136b05aa77ed
Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.
src/ZF/indrule.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/indrule.ML	Wed May 03 17:22:18 1995 +0200
+++ b/src/ZF/indrule.ML	Wed May 03 17:30:36 1995 +0200
@@ -189,7 +189,7 @@
 val fsplit_tac =
     REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, 
 			      dtac Pr.fsplitD,
-			      etac Pr.fsplitE,
+			      etac Pr.fsplitE,	(*apparently never used!*)
 			      bound_hyp_subst_tac]))
     THEN prune_params_tac;
isabelle