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.
removed debug output
authortraytel
Thu, 18 Aug 2016 13:12:53 +0200
changeset 63715 ad2c003782f9
parent 63714 b62f4f765353
child 63716 91a0494d8a4a
removed debug output
src/HOL/Tools/coinduction.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/coinduction.ML	Thu Aug 18 11:10:07 2016 +0200
+++ b/src/HOL/Tools/coinduction.ML	Thu Aug 18 13:12:53 2016 +0200
@@ -50,7 +50,7 @@
           SOME raw_thms => raw_thms
         | NONE => goal |> Logic.strip_assums_concl |> find_coinduct);
       val thy = Proof_Context.theory_of ctxt;
-      val concl = Variable.focus NONE goal ctxt |> fst |> snd |> Logic.strip_imp_concl |> @{print};
+      val concl = Variable.focus NONE goal ctxt |> fst |> snd |> Logic.strip_imp_concl;
       val raw_thm = (case find_first (fn thm =>
             Pattern.matches thy (Thm.concl_of thm, concl)) raw_thms of
           SOME thm => thm
isabelle