# HG changeset patch # User oheimb # Date 845390404 -7200 # Node ID 2bfc0675c92ff842f31d4049af9813f2a2a407a7 # Parent 076a8d2f972b8ccc44a0d15f39b435d063b0d0f5 corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25) diff -r 076a8d2f972b -r 2bfc0675c92f src/HOL/simpdata.ML --- 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]);