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.
declare impE iffD1 iffD2 ad elim of Pure;
authorwenzelm
Fri, 12 Oct 2001 12:11:39 +0200
changeset 11734 7a21bf539412
parent 11733 9dd88f3aa8e0
child 11735 60c0fa10bfc2
declare impE iffD1 iffD2 ad elim of Pure;
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/IFOL.thy	Fri Oct 12 12:10:07 2001 +0200
+++ b/src/FOL/IFOL.thy	Fri Oct 12 12:11:39 2001 +0200
@@ -119,6 +119,9 @@
 
 setup Simplifier.setup
 use "IFOL_lemmas.ML"
+
+declare impE [Pure.elim]  iffD1 [Pure.elim]  iffD2 [Pure.elim]
+
 use "fologic.ML"
 use "hypsubstdata.ML"
 setup hypsubst_setup
isabelle