Changed the type of Quot_True, so that it is an HOL constant.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 12 Apr 2010 13:19:28 +0200
changeset 36116 a6eab3be095b
parent 36115 6601c227c5bf
child 36117 01a9db7382f5
Changed the type of Quot_True, so that it is an HOL constant.
src/HOL/Quotient.thy
--- 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"