Corrected o_assoc lemma
authorpusch
Wed, 17 Jul 1996 17:15:54 +0200
changeset 1874 35f22792aade
parent 1873 b07ee188f061
child 1875 54c0462f8fb2
Corrected o_assoc lemma
src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jul 17 17:12:33 1996 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 17 17:15:54 1996 +0200
@@ -203,5 +203,5 @@
   "f(if c then x else y) = (if c then f x else f y)" 
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
 
-qed_goalw "o_assoc" HOL.thy [o_def] "(f o g) o h = (f o g o h)"
+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]);