equal
deleted
inserted
replaced
91 |
91 |
92 signature FAST_LIN_ARITH = |
92 signature FAST_LIN_ARITH = |
93 sig |
93 sig |
94 val prems_lin_arith_tac: Proof.context -> int -> tactic |
94 val prems_lin_arith_tac: Proof.context -> int -> tactic |
95 val lin_arith_tac: Proof.context -> int -> tactic |
95 val lin_arith_tac: Proof.context -> int -> tactic |
96 val lin_arith_simproc: Proof.context -> cterm -> thm option |
96 val lin_arith_simproc: Simplifier.proc |
97 val map_data: |
97 val map_data: |
98 ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
98 ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
99 lessD: thm list, neqE: thm list, simpset: simpset, |
99 lessD: thm list, neqE: thm list, simpset: simpset, |
100 number_of: (Proof.context -> typ -> int -> cterm) option} -> |
100 number_of: (Proof.context -> typ -> int -> cterm) option} -> |
101 {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
101 {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |