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.
corrected `correction` of o_assoc (of version 1.14),
authoroheimb
Tue, 15 Oct 1996 16:40:04 +0200
changeset 2098 2bfc0675c92f
parent 2097 076a8d2f972b
child 2099 c5f004bfcbab
corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/simpdata.ML	Tue Oct 15 16:32:59 1996 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 15 16:40:04 1996 +0200
@@ -328,7 +328,7 @@
 bind_thm ("o_apply", o_apply);
 
 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
-  (fn _=>[rtac ext 1, rtac refl 1]);
+  (fn _ => [rtac ext 1, rtac refl 1]);
isabelle