190 Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
190 Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
191 |
191 |
192 where a coercion is inserted in the second component and |
192 where a coercion is inserted in the second component and |
193 |
193 |
194 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
194 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
195 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, |
195 "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, |
196 Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
196 Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"} |
197 |
197 |
198 where it is not (since it is already constructed by a meta-implication). |
198 where it is not (since it is already constructed by a meta-implication). |
199 The purpose of the @{text "Trueprop"}-coercion is to embed formulae of |
199 The purpose of the @{text "Trueprop"}-coercion is to embed formulae of |
200 an object logic, for example HOL, into the meta-logic of Isabelle. The coercion |
200 an object logic, for example HOL, into the meta-logic of Isabelle. The coercion |
201 is needed whenever a term is constructed that will be proved as a theorem. |
201 is needed whenever a term is constructed that will be proved as a theorem. |