| changeset 2098 | 2bfc0675c92f |
| parent 2097 | 076a8d2f972b |
| child 2129 | 2ffe6e24f38d |
--- 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]);