equal
deleted
inserted
replaced
292 "Const \<dots> $ |
292 "Const \<dots> $ |
293 Abs (\"x\", \<dots>, |
293 Abs (\"x\", \<dots>, |
294 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
294 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
295 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
295 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
296 |
296 |
297 As can be seen, in the first case the arguments are correctly used, while in the |
297 As can be seen, in the first case the arguments are correctly used, while the |
298 second the @{term "P"} and @{text "Q"} from the antiquotation. |
298 second generates a term involving the @{term "P"} and @{text "Q"} from the |
|
299 antiquotation. |
299 |
300 |
300 One tricky point in constructing terms by hand is to obtain the |
301 One tricky point in constructing terms by hand is to obtain the |
301 fully qualified name for constants. For example the names for @{text "zero"} and |
302 fully qualified name for constants. For example the names for @{text "zero"} and |
302 @{text "+"} are more complex than one first expects, namely |
303 @{text "+"} are more complex than one first expects, namely |
303 |
304 |