# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260795459 -3600
# Node ID 76e34dd930f68f8255b0941ff55918ea4872bb4b
# Parent  5ef8be0175f637dada2c83f2be5c1d4be0f51a27# Parent  33ede8bb5fe1a27f70b762432da058157c8b9d05
merge.

diff -r 5ef8be0175f6 -r 76e34dd930f6 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Mon Dec 14 13:56:24 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Dec 14 13:57:39 2009 +0100
@@ -280,7 +280,7 @@
 sorry
 
 thm card_raw_cons_gt_0
-(*thm mem_card_raw_not_0*)
+thm mem_card_raw_gt_0
 thm not_nil_equiv_cons
 thm delete_raw.simps
 (*thm mem_delete_raw*)
diff -r 5ef8be0175f6 -r 76e34dd930f6 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 14 13:56:24 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 13:57:39 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
@@ -719,6 +720,8 @@
            (rtac inst_thm THEN' quotient_tac ctxt) i
          end
          handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *)
+(* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac
+   so I suppose it is equivalent to a "SOLVES" around quotient_tac. *)
     | _ => no_tac)
 *}