equal
deleted
inserted
replaced
20 |
20 |
21 |
21 |
22 *** Document preparation *** |
22 *** Document preparation *** |
23 |
23 |
24 * Antiquotation @{lemma} now imitates a regular terminal proof, |
24 * Antiquotation @{lemma} now imitates a regular terminal proof, |
25 demanding keyword 'by' and supporting the full method expressions. |
25 demanding keyword 'by' and supporting the full method expression |
|
26 syntax. |
26 |
27 |
27 |
28 |
28 *** HOL *** |
29 *** HOL *** |
29 |
30 |
30 * Methods "case_tac" and "induct_tac" now refer to the very same rules |
31 * Methods "case_tac" and "induct_tac" now refer to the very same rules |
74 resort for legacy applications. |
75 resort for legacy applications. |
75 |
76 |
76 * Antiquotations: block-structured compilation context indicated by |
77 * Antiquotations: block-structured compilation context indicated by |
77 \<lbrace> ... \<rbrace>; additional antiquotation forms: |
78 \<lbrace> ... \<rbrace>; additional antiquotation forms: |
78 |
79 |
79 @{let ?pat = term} - term abbreviation |
80 @{let ?pat = term} - term abbreviation (HO matching) |
80 @{note name = fact} - fact abbreviation |
81 @{note name = fact} - fact abbreviation |
81 @{thm name [attribs]} - singleton fact |
82 @{thm fact} - singleton fact |
82 @{thms name [attribs]} - general fact |
83 @{thms fact} - general fact |
83 @{lemma prop by method} - singleton goal |
84 @{lemma prop by method} - singleton goal |
84 @{lemma prop1 ... propN by method} - general goal |
85 @{lemma prop1 ... propN by method} - general goal |
85 |
86 |
86 |
87 |
87 |
88 |
88 |
89 |
89 New in Isabelle2008 (June 2008) |
90 New in Isabelle2008 (June 2008) |