Mercurial Mercurial > hg > isabelle-cookbook / 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.
updated to new Isabelle
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Fri, 17 May 2013 11:01:55 +0100
changeset 545 4a1539a2c18e
parent 544 501491d56798
child 546 d84867127c5d
updated to new Isabelle
ProgTutorial/antiquote_setup.ML file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- a/ProgTutorial/antiquote_setup.ML	Fri Apr 19 11:09:18 2013 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Fri May 17 11:01:55 2013 +0100
@@ -156,7 +156,7 @@
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
   val state = proof_state node
-  val goals = Goal_Display.pretty_goal {main = false, limit = false} ctxt state
+  val goals = Goal_Display.pretty_goal ctxt state
 
   val {prop, ...} = rep_thm state;
   val (As, _) = Logic.strip_horn prop;
Binary file progtutorial.pdf has changed
isabelle-cookbook