# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263291938 -3600
# Node ID d2fa1cf989319a7e1f9fc95b81a8a29d2b16c52d
# Parent  2480fb2a5e4eea404f4ca9060e341331a87afb88
Updated some comments.

diff -r 2480fb2a5e4e -r d2fa1cf98931 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 12 11:25:38 2010 +0100
@@ -298,27 +298,26 @@
     | _ => no_tac)
 
 
-(* FIXME / TODO needs to be adapted *)
 (*
-To prove that the regularised theorem implies the abs/rep injected, 
+To prove that the regularised theorem implies the abs/rep injected,
 we try:
 
- 1) theorems 'trans2' from the appropriate Quot_Type
- 2) remove lambdas from both sides: lambda_rsp_tac
- 3) remove Ball/Bex from the right hand side
- 4) use user-supplied RSP theorems
- 5) remove rep_abs from the right side
- 6) reflexivity of equality
- 7) split applications of lifted type (apply_rsp)
- 8) split applications of non-lifted type (cong_tac)
- 9) apply extentionality
- A) reflexivity of the relation
- B) assumption
+ The deterministic part:
+ -) remove lambdas from both sides
+ -) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
+ -) prove Ball/Bex relations unfolding fun_rel_id
+ -) reflexivity of equality
+ -) prove equality of relations using equals_rsp
+ -) use user-supplied RSP theorems
+ -) solve 'relation of relations' goals using quot_rel_rsp
+ -) remove rep_abs from the right side
     (Lambdas under respects may have left us some assumptions)
- C) proving obvious higher order equalities by simplifying fun_rel
-    (not sure if it is still needed?)
- D) unfolding lambda on one side
- E) simplifying (= ===> =) for simpler respectfulness
+ Then in order:
+ -) split applications of lifted type (apply_rsp)
+ -) split applications of non-lifted type (cong_tac)
+ -) apply extentionality
+ -) assumption
+ -) reflexivity of the relation
 *)