From ee0b2d8f1807f88af0ae0683908ffbfc78c4f34b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 25 May 2005 13:46:11 +0000
Subject: [PATCH] fix

---
 helm/matita/tests/apply.ma | 24 ++++++++++++++++++++++++
 helm/matita/tests/simpl.ma |  2 +-
 2 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 helm/matita/tests/apply.ma

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
new file mode 100644
index 000000000..9e8663517
--- /dev/null
+++ b/helm/matita/tests/apply.ma
@@ -0,0 +1,24 @@
+%% test _with_ the WHD on the apply argument
+
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+
+theorem b:
+  \forall x:Prop.
+  (not x) \to x \to False.
+intro.
+apply H.
+assumption.
+qed.
+
+%% test _without_ the WHD on the apply argument
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem a:
+  \forall A:Set.
+  \forall x,y : A.
+  not (x=y) \to not (x=y).
+intro.
+apply H.
+qed.
diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 887566f58..c455b7692 100644
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -5,4 +5,4 @@ theorem a :
  \forall x,y : A.
  not (x = y) \to not(y = x).
 intro.
-simplify in hyp not(x=y).
+simplify.
-- 
2.39.2