1.1 --- a/src/HOL/WF_Rel.ML Wed Mar 22 13:22:39 2000 +0100
1.2 +++ b/src/HOL/WF_Rel.ML Wed Mar 22 13:23:57 2000 +0100
1.3 @@ -101,7 +101,7 @@
1.4 by (rtac (wf_measure RS wf_subset) 1);
1.5 by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
1.6 symmetric less_def])1);
1.7 -by (fast_tac (claset() addSIs [psubset_card]) 1);
1.8 +by (fast_tac (claset() addSEs [psubset_card]) 1);
1.9 qed "wf_finite_psubset";
1.10
1.11 Goalw [finite_psubset_def, trans_def] "trans finite_psubset";