# HG changeset patch # User paulson # Date 956482866 -7200 # Node ID 981ebe7f1f103e3b381c85c64a314693bb7fb554 # Parent 9f18aba48519b43132023f6efe49deb7c9681b06 [Int_CC.sum_conv, Int_CC.rel_conv] no longer exist diff -r 9f18aba48519 -r 981ebe7f1f10 src/HOL/UNITY/Lift.ML --- 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*)