changeset 8769 | 981ebe7f1f10 |
parent 7403 | c318acb88251 |
child 8777 | 0c1061ea7559 |
--- a/src/HOL/UNITY/Lift.ML Sun Apr 23 11:39:56 2000 +0200 +++ b/src/HOL/UNITY/Lift.ML Sun Apr 23 11:41:06 2000 +0200 @@ -224,9 +224,7 @@ by (Blast_tac 1); qed "E_thm16a"; -(*Must sometimes delete them because they introduce multiplication*) -val metric_ss = simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv] - addsimps metric_simps; +val metric_ss = simpset() addsimps metric_simps; (*lem_lift_5_1 has ~goingup instead of goingdown*)