| changeset 6128 | 2acc5d36610c |
| parent 5983 | 79e301a6a51b |
| child 6707 | 3b07e62a718c |
--- a/src/HOL/UNITY/LessThan.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/UNITY/LessThan.ML Thu Jan 14 13:18:09 1999 +0100 @@ -7,10 +7,6 @@ *) -(*Make Auto_tac and Force_tac try lin_arith_tac!*) -claset_ref() := claset() addaltern ("lin_arith_tac",Fast_Nat_Arith.lin_arith_tac); - - (*** lessThan ***) Goalw [lessThan_def] "(i: lessThan k) = (i<k)";