changeset 5983 | 79e301a6a51b |
parent 5706 | 21706a735c8d |
child 6536 | 281d44905cab |
--- a/src/HOL/UNITY/Mutex.ML Fri Nov 27 16:54:59 1998 +0100 +++ b/src/HOL/UNITY/Mutex.ML Fri Nov 27 17:00:30 1998 +0100 @@ -69,10 +69,6 @@ simpset_of Int.thy addsimps [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, integ_of_BIT])); -by (exhaust_tac "na" 1); -by (exhaust_tac "nat" 2); -by (exhaust_tac "n" 3); -by Auto_tac; qed "eq_123";