# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272614664 -7200
# Node ID abada9e6f943772b3cf196e063e1e38ea869821a
# Parent  b7a89b043d51201ff1afad890fc550ae8527ee53
qpaper

diff -r b7a89b043d51 -r abada9e6f943 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Apr 29 17:52:33 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Fri Apr 30 10:04:24 2010 +0200
@@ -3,6 +3,10 @@
 imports "Quotient" 
         "LaTeXsugar"
 begin
+
+notation (latex output)
+  fun_rel ("_ ===> _" [51, 51] 50)
+
 (*>*)
 
 section {* Introduction *}
@@ -60,6 +64,43 @@
 
 section {* Lifting Theorems *}
 
+text {* TBD *}
+
+text {* Why providing a statement to prove is necessary is some cases *}
+
+subsection {* Regularization *}
+
+text {*
+Transformation of the theorem statement:
+\begin{itemize}
+\item Quantifiers and abstractions involving raw types replaced by bounded ones.
+\item Equalities involving raw types replaced by bounded ones.
+\end{itemize}
+
+The procedure.
+
+Example of non-regularizable theorem ($0 = 1$).
+
+New regularization lemmas:
+\begin{lemma}
+If @{term R2} is an equivalence relation, then:
+\begin{eqnarray}
+@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
+@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
+\end{eqnarray}
+\end{lemma}
+
+*}
+
+subsection {* Injection *}
+
+subsection {* Cleaning *}
+
+text {* Preservation of quantifiers, abstractions, relations, quotient-constants
+  (definitions) and user given constant preservation lemmas *}
+
+section {* Examples *}
+
 section {* Related Work *}
 
 text {*