# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262684480 -3600
# Node ID 43336511993f8f6d563e50bf5658ec779503617f
# Parent  d193e2111811ca34897727740d2e0f9d29b8773f
Readded 'regularize_to_injection' which I believe will be needed.

diff -r d193e2111811 -r 43336511993f Unused.thy
--- 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)*)