--- a/Unused.thy	Sat Jan 02 23:15:15 2010 +0100
+++ b/Unused.thy	Tue Jan 05 10:41:20 2010 +0100
@@ -1,6 +1,13 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+lemma regularize_to_injection:
+  shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+  by(auto simp add: QUOT_TRUE_def)
+
+
+
+
 ML {*
   fun dest_cbinop t =
     let
@@ -123,4 +130,4 @@
         (* Not sure if the following context should not be used *)
         val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
-      in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)
\ No newline at end of file
+      in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)