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.
More robust proof (?)
authorpaulson
Fri, 21 Feb 1997 15:38:44 +0100
changeset 2673 1b266c161134
parent 2672 85d7e800d754
child 2674 4385d521a691
More robust proof (?)
src/ZF/upair.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/upair.ML	Fri Feb 21 15:31:47 1997 +0100
+++ b/src/ZF/upair.ML	Fri Feb 21 15:38:44 1997 +0100
@@ -167,7 +167,7 @@
 (*Classical introduction rule*)
 qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  (fn prems=>
-  [ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]);
+  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
 
 AddSIs [consCI];
 AddSEs [consE];
isabelle