| changeset 2493 | bdeb5024353a |
| parent 2469 | b50b8c0eec01 |
| child 2877 | 6476784dba1c |
--- a/src/ZF/pair.ML Wed Jan 08 15:03:53 1997 +0100 +++ b/src/ZF/pair.ML Wed Jan 08 15:04:27 1997 +0100 @@ -99,10 +99,10 @@ AddSEs [SigmaE2, SigmaE]; qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0" - (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]); + (fn _ => [ (Fast_tac 1) ]); qed_goal "Sigma_empty2" thy "A*0 = 0" - (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]); + (fn _ => [ (Fast_tac 1) ]); Addsimps [Sigma_empty1, Sigma_empty2];