Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
changeset 44928 7ef6505bde7f
parent 44919 482f1807976e
child 45166 861ab6f9eb2b 
--- a/src/HOL/Finite_Set.thy	Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Sep 14 10:08:52 2011 -0400
@@ -784,7 +784,7 @@
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?inf"
     by (induct A arbitrary: B)
-      (simp_all add: INFI_def inf_left_commute)
+      (simp_all add: INF_def inf_left_commute)
 qed
 
 lemma sup_SUPR_fold_sup:
@@ -795,7 +795,7 @@
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?sup"
     by (induct A arbitrary: B)
-      (simp_all add: SUPR_def sup_left_commute)
+      (simp_all add: SUP_def sup_left_commute)
 qed
 
 lemma INFI_fold_inf:
isabelle