X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fbool.ma;h=c9a86165a24f1aaea48b235d4f5b140df29a97db;hb=0e9f9d6d7a0466ee132553fb7a983eac282fb12f;hp=953471191b1ddb8b215c34998df0ed9822890c16;hpb=7bfd412f8023e814ef4b8da290e3c12ba71d5b80;p=helm.git diff --git a/helm/software/matita/library/datatypes/bool.ma b/helm/software/matita/library/datatypes/bool.ma index 953471191..c9a86165a 100644 --- a/helm/software/matita/library/datatypes/bool.ma +++ b/helm/software/matita/library/datatypes/bool.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/datatypes/bool/". - include "logic/equality.ma". include "higher_order_defs/functions.ma". @@ -37,7 +35,7 @@ unfold Not.intro. change with match true with [ true \Rightarrow False -| flase \Rightarrow True]. +| false \Rightarrow True]. rewrite > H.simplify.exact I. qed. @@ -196,4 +194,4 @@ intros. rewrite > H. rewrite > H1. reflexivity. -qed. \ No newline at end of file +qed.