Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
The missing rule.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 21 Jan 2010 09:02:04 +0100
changeset 907 e576a97e9a3e
parent 906 a394c7337966
child 908 1bf4337919d3
The missing rule.
Quot/QuotMain.thy file | annotate | diff | comparison | revisions 
--- 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)
nominal2