From 52497e1453862dc243cc76698972ae0c41812cec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2009 11:50:14 +0000 Subject: [PATCH] new syntax --- helm/software/matita/matita.lang | 43 ++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 2f71b5f7e..64229e793 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -22,6 +22,17 @@ variant axiom + + + ntheorem + nrecord + ndefinition + ninductive + ncoinductive + nlet + nlemma + naxiom + alias @@ -55,6 +66,13 @@ with + + unification + hint + ncoercion + nqed + + \[ @@ -84,6 +102,16 @@ CProp + + Prop + Type[0] + CProp[0] + Type[1] + CProp[1] + Type[2] + CProp[2] + + absurd apply @@ -164,6 +192,17 @@ rule + + napply + ncases + nletin + nauto + nelim + nwhd + nnormalize + nassumption + + try solve @@ -191,6 +230,10 @@ debug cr + + + ncheck +