[isabelle] LaTeXsugar



Dear Sugarers,

how about adding the following to LaTeXsugar.thy?

syntax (latex output)
  "_CollectIndex" ::
    "pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<^esub>)")

translations
  "_CollectIndex p i" <= "{p | i. CONST True}"


term "{f i | i. True}"

cheers

chris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.