| changeset 55 | 331d93292ee0 |
| parent 14 | 1c0926788772 |
| child 70 | 8a29f8b4aca1 |
--- a/src/ZF/ind_syntax.ML Fri Oct 15 10:04:30 1993 +0100 +++ b/src/ZF/ind_syntax.ML Fri Oct 15 10:21:01 1993 +0100 @@ -172,4 +172,7 @@ val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b" (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); +(*Delete needless equality assumptions*) +val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P" + (fn _ => [assume_tac 1]);