equal
deleted
inserted
replaced
130 term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *} |
130 term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *} |
131 term "Suc 0" -- {* successor of 0, in other words 1::nat *} |
131 term "Suc 0" -- {* successor of 0, in other words 1::nat *} |
132 term "Lam [x].Var x" -- {* a lambda-term *} |
132 term "Lam [x].Var x" -- {* a lambda-term *} |
133 term "App t1 t2" -- {* another lambda-term *} |
133 term "App t1 t2" -- {* another lambda-term *} |
134 term "x::name" -- {* an (object) variable of type name *} |
134 term "x::name" -- {* an (object) variable of type name *} |
135 term "atom (x::name)" -- {* atom is an overloded function *} |
135 term "atom (x::name)" -- {* atom is an overloaded function *} |
136 |
136 |
137 text {* |
137 text {* |
138 Lam [x].Var is the syntax we made up for lambda abstractions. If you |
138 Lam [x].Var is the syntax we made up for lambda abstractions. If you |
139 prefer, you can have your own syntax (but \<lambda> is already taken up for |
139 prefer, you can have your own syntax (but \<lambda> is already taken up for |
140 Isabelle's functions). We also came up with the type "name" for variables. |
140 Isabelle's functions). We also came up with the type "name" for variables. |
393 |
393 |
394 text {* |
394 text {* |
395 Just like gotos in the Basic programming language, labels often reduce |
395 Just like gotos in the Basic programming language, labels often reduce |
396 the readability of proofs. Therefore one can use in Isar the notation |
396 the readability of proofs. Therefore one can use in Isar the notation |
397 "then have" in order to feed a have-statement to the proof of |
397 "then have" in order to feed a have-statement to the proof of |
398 the next have-statement. This is used in teh second case below. |
398 the next have-statement. This is used in the second case below. |
399 *} |
399 *} |
400 |
400 |
401 |
401 |
402 |
402 |
403 text {* |
403 text {* |
404 The label ih2 cannot be got rid of in this way, because it is used |
404 The label ih2 cannot be got rid of in this way, because it is used |
405 two lines below and we cannot rearange them. We can still avoid the |
405 two lines below and we cannot rearrange them. We can still avoid the |
406 label by feeding a sequence of facts into a proof using the |
406 label by feeding a sequence of facts into a proof using the |
407 "moreover"-chaining mechanism: |
407 "moreover"-chaining mechanism: |
408 |
408 |
409 have "statement_1" \<dots> |
409 have "statement_1" \<dots> |
410 moreover |
410 moreover |