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.
reintroduced two-line-per-inference Isar proof format
authorblanchet
Thu, 28 Aug 2014 00:40:37 +0200
changeset 58054 1d9edd486479
parent 58053 decb3e2528e7
child 58055 625bdd5c70b2
reintroduced two-line-per-inference Isar proof format
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 00:40:19 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Aug 28 00:40:37 2014 +0200
@@ -340,7 +340,7 @@
           | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
         #> add_str (of_label l)
         #> add_term t
-        #> add_str (" " ^ of_method ls ss meth ^
+        #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
           (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
isabelle