# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260782367 -3600
# Node ID 33ede8bb5fe1a27f70b762432da058157c8b9d05
# Parent  7092bd4fd26431630247248c457508debca74609
reply to question in code

diff -r 7092bd4fd264 -r 33ede8bb5fe1 Quot/QuotMain.thy
--- 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