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.
tuned
authorsmolkas
Thu, 11 Jul 2013 13:33:19 +0200
changeset 52590 02713cd2c2cd
parent 52589 d28d2d89034d
child 52591 760a567f1609
tuned
src/HOL/Tools/Sledgehammer/sledgehammer_print.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_print.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -20,8 +20,8 @@
     Proof of fix * assms * isar_step list
   and isar_step =
     Let of term * term |
-  (* for |fix|>0, this is an obtain step; step may contain subproofs *)
-  Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
+    (* for |fix|>0, this is an obtain step; step may contain subproofs *)
+    Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
   and byline =
     By_Metis of facts
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jul 11 11:40:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jul 11 13:33:19 2013 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
isabelle