src/Doc/Isar_Ref/Document_Preparation.thy
changeset 68481 fb6afa538b04
parent 67297 86a099f896fc
child 68484 59793df7f853
equal deleted inserted replaced
68480:27be5b4cb80d 68481:fb6afa538b04
   165   %% FIXME less monolithic presentation, move to individual sections!?
   165   %% FIXME less monolithic presentation, move to individual sections!?
   166   @{rail \<open>
   166   @{rail \<open>
   167     @{syntax_def antiquotation_body}:
   167     @{syntax_def antiquotation_body}:
   168       (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
   168       (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
   169         options @{syntax text} |
   169         options @{syntax text} |
   170       @@{antiquotation theory} options @{syntax name} |
   170       @@{antiquotation theory} options @{syntax embedded} |
   171       @@{antiquotation thm} options styles @{syntax thms} |
   171       @@{antiquotation thm} options styles @{syntax thms} |
   172       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
   172       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
   173       @@{antiquotation prop} options styles @{syntax prop} |
   173       @@{antiquotation prop} options styles @{syntax prop} |
   174       @@{antiquotation term} options styles @{syntax term} |
   174       @@{antiquotation term} options styles @{syntax term} |
   175       @@{antiquotation (HOL) value} options styles @{syntax term} |
   175       @@{antiquotation (HOL) value} options styles @{syntax term} |