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/Pure/Isar/proof.ML
changeset 67721 5348bea4accd
parent 67713 041898537c19
child 67932 04352338f7f3 
--- a/src/Pure/Isar/proof.ML	Sun Feb 25 12:59:08 2018 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Feb 25 15:44:46 2018 +0100
@@ -171,7 +171,7 @@
    {statement: (string * Position.T) * term list list * term,
       (*goal kind and statement (starting with vars), initial proposition*)
     using: thm list,                      (*goal facts*)
-    goal: thm,                            (*subgoals ==> statement*)
+    goal: thm,                            (*subgoals \<Longrightarrow> statement*)
     before_qed: Method.text option,
     after_qed:
       (context * thm list list -> state -> state) *
isabelle