src/HOL/Quotient.thy
changeset 36116 a6eab3be095b
parent 35827 f552152d7747
child 36123 7f877bbad5b2
     1.1 --- a/src/HOL/Quotient.thy	Sun Apr 11 17:46:42 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Mon Apr 12 13:19:28 2010 +0200
     1.3 @@ -747,7 +747,7 @@
     1.4    about the lifted theorem in a tactic.
     1.5  *}
     1.6  definition
     1.7 -  "Quot_True x \<equiv> True"
     1.8 +  "Quot_True (x :: 'a) \<equiv> True"
     1.9  
    1.10  lemma
    1.11    shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"