Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
less_imp_diff_positive is redundant with new simprule zero_less_diff
authorpaulson
Wed, 19 Aug 1998 10:26:37 +0200
changeset 5334 68e5eeee4e59
parent 5333 ea33e66dcedd
child 5335 07fb8999de62
less_imp_diff_positive is redundant with new simprule zero_less_diff
src/HOL/Divides.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Divides.ML	Wed Aug 19 10:26:02 1998 +0200
+++ b/src/HOL/Divides.ML	Wed Aug 19 10:26:37 1998 +0200
@@ -228,7 +228,6 @@
  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
- by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
 (* case n=m *)
 by (subgoal_tac "m=n" 1);
isabelle