| changeset 55029 | 61a6bf7d4b02 |
| parent 54883 | dd04a8b654fc |
| child 55112 | b1a5d603fd12 |
| 55028:00e849f5b397 | 55029:61a6bf7d4b02 |
|---|---|
789 ; |
789 ; |
790 @@{ML_antiquotation thm} thmref |
790 @@{ML_antiquotation thm} thmref |
791 ; |
791 ; |
792 @@{ML_antiquotation thms} thmrefs |
792 @@{ML_antiquotation thms} thmrefs |
793 ; |
793 ; |
794 @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\ |
794 @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline> |
795 @'by' method method? |
795 @'by' method method? |
796 "} |
796 "} |
797 |
797 |
798 \begin{description} |
798 \begin{description} |
799 |
799 |