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.
ACe_axioms;
authorwenzelm
Thu, 18 Jul 2002 12:08:45 +0200
changeset 13390 c48c634605f1
parent 13389 0cbda884a7e5
child 13391 553e7b62680f
ACe_axioms;
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite_Set.thy	Thu Jul 18 12:05:51 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 18 12:08:45 2002 +0200
@@ -720,7 +720,7 @@
     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   apply (induct set: Finites)
    apply simp
-  apply (simp add: AC ACe.axioms ACe_axioms_def
+  apply (simp add: AC ACe_axioms ACe_axioms_def
     LC_axioms_def LC.fold_insert insert_absorb Int_insert_left)
   done
isabelle