Haftungsausschluß.mlg KontaktPVS {PVS[61] Isabelle[72] Cobol[94]}diese Dinge liegen außhalb unserer Verantwortung
{
open Pcoq.Constr
}
GRAMMAR EXTEND Gram
GLOBAL: operconstr;
operconstr: LEVEL "0"
[ [ s = QUOTATION "foobar:" ->
{
CAst.make ~loc (Constrexpr.CSort Glob_term.GProp) } ] ]
;
END
[ Seitenstruktur0.63Drucken
]
