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.
avoid noise (cf. 03ff4d1e6784);
authorwenzelm
Fri, 31 Oct 2014 16:56:23 +0100
changeset 58847 c44aff8ac894
parent 58846 98c03412079b
child 58848 fd0c85d7da38
avoid noise (cf. 03ff4d1e6784);
src/HOL/Divides.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Divides.thy	Fri Oct 31 16:03:45 2014 +0100
+++ b/src/HOL/Divides.thy	Fri Oct 31 16:56:23 2014 +0100
@@ -2047,8 +2047,8 @@
   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
   val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
-  fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
-    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
+  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
   fun binary_proc proc ctxt ct =
     (case Thm.term_of ct of
       _ $ t $ u =>
isabelle