Mercurial Mercurial > hg > nominal2 / 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.
reply to question in code
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 14 Dec 2009 10:19:27 +0100
changeset 745 33ede8bb5fe1
parent 744 7092bd4fd264
child 747 76e34dd930f6
child 748 7e19c4b3ab0f
reply to question in code
Quot/QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/Quot/QuotMain.thy	Mon Dec 14 10:12:23 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 10:19:27 2009 +0100
@@ -660,7 +660,8 @@
 
 ML {*
 (* FIXME / TODO: what is asmf and asma in the code below *)
-
+(* asmf is the QUOT_TRUE assumption function
+   asma are    QUOT_TRUE assumption arguments *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   let
nominal2