# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264060924 -3600
# Node ID e576a97e9a3e225aab62ae3fb25dd23308068d26
# Parent  a394c73379664120245e20a7255c1852aee3a25c
The missing rule.

diff -r a394c7337966 -r e576a97e9a3e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Jan 21 07:38:34 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 21 09:02:04 2010 +0100
@@ -138,6 +138,7 @@
 lemma 
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
+  and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"
   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
 by (simp_all add: Quot_True_def ext)