author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 12 Apr 2010 13:19:28 +0200 | |
changeset 36116 | a6eab3be095b |
parent 36115 | 6601c227c5bf |
child 36117 | 01a9db7382f5 |
--- 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"