Yet another semantics for simplify.

[helm.git] / helm / matita / library / datatypes / bool.ma

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index 11f1d7a8c49d48047e12caaeec555c207e1ca784..f4aec8167476b0d88204a06d3d23aaa798a323ac 100644 (file)
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -32,7 +32,7 @@ theorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
 qed.
 
 theorem not_eq_true_false : true \neq false.
-simplify.intro.
+unfold Not.intro.
 change with 
 match true with
 [ true \Rightarrow False