EXPERIMENTAL COMMIT (part B, by CSC :-):

[helm.git] / helm / software / matita / tests / ng_include.ma

diff --git a/helm/software/matita/tests/ng_include.ma b/helm/software/matita/tests/ng_include.ma
index 4584afddcd5eb3f17fd66ada30724c850a7d2911..2582da4b418f95d649915105f6589e594aa17a60 100644 (file)
--- a/helm/software/matita/tests/ng_include.ma
+++ b/helm/software/matita/tests/ng_include.ma
@@ -24,4 +24,8 @@ axiom P: nat → Prop.
 
 unification hint 0 (∀n. P (0 + n) = P n) .
 
-ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p.
\ No newline at end of file
+ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p → True.
+ #n; #H; #p; #_; napply I;
+nqed. 
+
+naxiom nnn: nat.
\ No newline at end of file