Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed psubset_card -> psubset_card_mono
authorpaulson
Fri, 16 Jun 2000 13:16:07 +0200
changeset 9076 108ec332625d
parent 9075 e8521ed7f35b
child 9077 5bf9b0d6df8a
renamed psubset_card -> psubset_card_mono
src/HOL/WF_Rel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/WF_Rel.ML	Fri Jun 16 13:15:40 2000 +0200
+++ b/src/HOL/WF_Rel.ML	Fri Jun 16 13:16:07 2000 +0200
@@ -101,7 +101,7 @@
 by (rtac (wf_measure RS wf_subset) 1);
 by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
 				 symmetric less_def])1);
-by (fast_tac (claset() addSEs [psubset_card]) 1);
+by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
 qed "wf_finite_psubset";
 
 Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
isabelle