Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quotient.thy
changeset 36116 a6eab3be095b
parent 35827 f552152d7747
child 36123 7f877bbad5b2 
--- a/src/HOL/Quotient.thy	Sun Apr 11 17:46:42 2010 +0200
+++ b/src/HOL/Quotient.thy	Mon Apr 12 13:19:28 2010 +0200
@@ -747,7 +747,7 @@
   about the lifted theorem in a tactic.
 *}
 definition
-  "Quot_True x \<equiv> True"
+  "Quot_True (x :: 'a) \<equiv> True"
 
 lemma
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
isabelle