Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Ferrack.thy
changeset 32441 0273a2f787ea
parent 31952 40501bb2d57c
child 32642 026e7c6a6d08 
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 19:49:05 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 20:02:18 2009 +0200
@@ -512,7 +512,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
isabelle