equal
deleted
inserted
replaced
20 Context.generic |
20 Context.generic |
21 val setup: Context.generic -> Context.generic |
21 val setup: Context.generic -> Context.generic |
22 val global_setup: theory -> theory |
22 val global_setup: theory -> theory |
23 val split_limit: int Config.T |
23 val split_limit: int Config.T |
24 val neq_limit: int Config.T |
24 val neq_limit: int Config.T |
25 val warning_count: int Unsynchronized.ref |
|
26 val trace: bool Unsynchronized.ref |
25 val trace: bool Unsynchronized.ref |
27 end; |
26 end; |
28 |
27 |
29 structure Lin_Arith: LIN_ARITH = |
28 structure Lin_Arith: LIN_ARITH = |
30 struct |
29 struct |
795 |
794 |
796 |
795 |
797 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; |
796 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; |
798 val lin_arith_tac = Fast_Arith.lin_arith_tac; |
797 val lin_arith_tac = Fast_Arith.lin_arith_tac; |
799 val trace = Fast_Arith.trace; |
798 val trace = Fast_Arith.trace; |
800 val warning_count = Fast_Arith.warning_count; |
|
801 |
799 |
802 (* reduce contradictory <= to False. |
800 (* reduce contradictory <= to False. |
803 Most of the work is done by the cancel tactics. *) |
801 Most of the work is done by the cancel tactics. *) |
804 |
802 |
805 val init_arith_data = |
803 val init_arith_data = |