changeset 3323 | 194ae2e0c193 |
parent 2640 | ee4dfce170a0 |
child 3842 | b55686a7b22c |
--- a/src/HOLCF/Sprod2.ML Fri May 23 18:55:28 1997 +0200 +++ b/src/HOLCF/Sprod2.ML Sun May 25 11:07:52 1997 +0200 @@ -12,7 +12,7 @@ qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)" (fn prems => [ - (fold_goals_tac [po_def,less_sprod_def]), + (fold_goals_tac [less_sprod_def]), (rtac refl 1) ]);