| changeset 1874 | 35f22792aade |
| parent 1821 | bc506bcb9fe4 |
| child 1892 | 23765bc3e8e2 |
--- 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]);