equal
deleted
inserted
replaced
326 (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
326 (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
327 |
327 |
328 bind_thm ("o_apply", o_apply); |
328 bind_thm ("o_apply", o_apply); |
329 |
329 |
330 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" |
330 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h" |
331 (fn _=>[rtac ext 1, rtac refl 1]); |
331 (fn _ => [rtac ext 1, rtac refl 1]); |
332 |
332 |
333 |
333 |
334 |
334 |
335 |
335 |
336 (*** Install simpsets and datatypes in theory structure ***) |
336 (*** Install simpsets and datatypes in theory structure ***) |