src/HOL/Tools/lin_arith.ML
changeset 32863 5e8cef567042
parent 32740 9dd0a2f83429
child 33035 15eab423e573
equal deleted inserted replaced
32862:1fc86cec3bdf 32863:5e8cef567042
   765 
   765 
   766 val pre_tac = LA_Data.pre_tac;
   766 val pre_tac = LA_Data.pre_tac;
   767 
   767 
   768 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
   768 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
   769 
   769 
   770 val map_data = Fast_Arith.map_data;
       
   771 
       
   772 fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   770 fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   773   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
   771   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
   774     lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
   772     lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
   775 
   773 
   776 fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   774 fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =