changeset 19798 | 94f12468bbba |
parent 15570 | 8d8c70b41bab |
child 21646 | c07b5b0e8492 |
--- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 06 20:42:27 2006 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 06 20:42:28 2006 +0200 @@ -103,7 +103,7 @@ \ (allI % TYPE('a) % P %% \ \ (Lam x. \ \ iffD2 % P x % Q x %% (prf % x) %% \ - \ (spec % TYPE('a) % ?Q % x %% prf')))", + \ (spec % TYPE('a) % Q % x %% prf')))", (* Ex *)