# HG changeset patch
# User paulson
# Date 827836697 -3600
# Node ID e15e8c0c1e37357576e689f2708a3bfb5a3a7689
# Parent  5c123831c4e274eeebf14c0bdc378fc14ffb4520
Added two of KGs rules

diff -r 5c123831c4e2 -r e15e8c0c1e37 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Tue Mar 26 11:33:13 1996 +0100
+++ b/src/FOL/IFOL.ML	Tue Mar 26 11:38:17 1996 +0100
@@ -358,8 +358,24 @@
  (fn major::prems=>
   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
 
-(*Courtesy Krzysztof Grabczewski*)
+(*** Courtesy of Krzysztof Grabczewski ***)
+
 val major::prems = goal IFOL.thy "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
 by (rtac (major RS disjE) 1);
 by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
 qed "disj_imp_disj";
+
+(* The following two theorms are useful when rewriting only one instance  *) 
+(* of a definition                                                        *)
+(* first one for definitions of formulae and the second for terms         *)
+
+val prems = goal IFOL.thy "(A == B) ==> A <-> B";
+by (rewrite_goals_tac prems);
+by (rtac iff_refl 1);
+qed "def_imp_iff";
+
+val prems = goal IFOL.thy "(A == B) ==> A = B";
+by (rewrite_goals_tac prems);
+by (rtac refl 1);
+qed "def_imp_eq";
+