changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 11868 | 56db9f3a6b3e |
--- a/src/HOL/UNITY/Union.ML Fri Oct 05 23:58:52 2001 +0200 +++ b/src/HOL/UNITY/Union.ML Sat Oct 06 00:02:46 2001 +0200 @@ -352,7 +352,7 @@ bind_thm ("ok_sym", ok_commute RS iffD1); -Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)"; +Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"; by (asm_full_simp_tac (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);