From 23043db144b24b8cd2072800b61137bb396f891e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Feb 2009 20:50:20 +0000 Subject: [PATCH] some work to speed up the system --- .../formal_topology/overlap/basic_pairs.ma | 81 ++++++++++++++----- .../overlap/basic_pairs_to_o-basic_pairs.ma | 57 ++++++++++--- .../formal_topology/overlap/o-basic_pairs.ma | 80 +++++++++++++----- .../overlap/r-o-basic_pairs.ma | 46 +++-------- helm/software/matita/dist/ChangeLog | 3 + 5 files changed, 184 insertions(+), 83 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma index 84f48c894..c5546477b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -88,11 +88,11 @@ definition id_relation_pair: ∀o:basic_pair. relation_pair o o. apply (H1 \sup -1);] qed. -definition relation_pair_composition: - ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). - intros; - constructor 1; - [ intros (r r1); +lemma relation_pair_composition: + ∀o1,o2,o3: basic_pair. + relation_pair_setoid o1 o2 → relation_pair_setoid o2 o3 → relation_pair_setoid o1 o3. +intros 3 (o1 o2 o3); + intros (r r1); constructor 1; [ apply (r1 \sub\c ∘ r \sub\c) | apply (r1 \sub\f ∘ r \sub\f) @@ -106,7 +106,17 @@ definition relation_pair_composition: apply (.= ASSOC ^ -1); apply (.= H‡#); apply ASSOC] - | intros; +qed. + +lemma relation_pair_composition_is_morphism: + ∀o1,o2,o3: basic_pair. + ∀a,a':relation_pair_setoid o1 o2. + ∀b,b':relation_pair_setoid o2 o3. + a=a' → b=b' → + relation_pair_composition o1 o2 o3 a b + = relation_pair_composition o1 o2 o3 a' b'. +intros 3 (o1 o2 o3); + intros; change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c)); change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); @@ -117,29 +127,64 @@ definition relation_pair_composition: apply (.= e‡#); apply (.= ASSOC); apply (.= #‡(commute ?? b')\sup -1); - apply (ASSOC ^ -1)] + apply (ASSOC ^ -1); qed. - -definition BP: category1. + +definition relation_pair_composition_morphism: + ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). + intros; constructor 1; - [ apply basic_pair - | apply relation_pair_setoid - | apply id_relation_pair - | apply relation_pair_composition - | intros; + [ apply relation_pair_composition; + | apply relation_pair_composition_is_morphism;] +qed. + +lemma relation_pair_composition_morphism_assoc: +Πo1:basic_pair +.Πo2:basic_pair + .Πo3:basic_pair + .Πo4:basic_pair + .Πa12:relation_pair_setoid o1 o2 + .Πa23:relation_pair_setoid o2 o3 + .Πa34:relation_pair_setoid o3 o4 + .relation_pair_composition_morphism o1 o3 o4 + (relation_pair_composition_morphism o1 o2 o3 a12 a23) a34 + =relation_pair_composition_morphism o1 o2 o4 a12 + (relation_pair_composition_morphism o2 o3 o4 a23 a34). + intros; change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); alias symbol "refl" = "refl1". alias symbol "prop2" = "prop21". apply (ASSOC‡#); - | intros; +qed. + +lemma relation_pair_composition_morphism_respects_id: + ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2. + relation_pair_composition_morphism o1 o1 o2 (id_relation_pair o1) a=a. + intros; change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_right1 ????)‡#); - | intros; + apply ((id_neutral_right1 ????)‡#); +qed. + +lemma relation_pair_composition_morphism_respects_id_r: + ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2. + relation_pair_composition_morphism o1 o2 o2 a (id_relation_pair o2)=a. + intros; change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_left1 ????)‡#);] + apply ((id_neutral_left1 ????)‡#); qed. +definition BP: category1. + constructor 1; + [ apply basic_pair + | apply relation_pair_setoid + | apply id_relation_pair + | apply relation_pair_composition_morphism + | apply relation_pair_composition_morphism_assoc; + | apply relation_pair_composition_morphism_respects_id; + | apply relation_pair_composition_morphism_respects_id_r;] +qed. + definition basic_pair_of_BP : objs1 BP → basic_pair ≝ λx.x. coercion basic_pair_of_BP. diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma index d8813fdc1..9e85452d5 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma @@ -39,12 +39,13 @@ definition o_relation_pair_of_relation_pair: | apply commute;]] qed. -definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). - constructor 1; - [ apply o_basic_pair_of_basic_pair; - | intros; constructor 1; - [ apply (o_relation_pair_of_relation_pair S T); - | intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify; +lemma o_relation_pair_of_relation_pair_is_morphism : + ∀S,T:category2_of_category1 BP. + ∀a,b:arrows2 (category2_of_category1 BP) S T.a=b → + (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T))) + (o_relation_pair_of_relation_pair S T a) (o_relation_pair_of_relation_pair S T b). +intros 2 (S T); + intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify; unfold o_basic_pair_of_basic_pair; simplify; [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); @@ -58,8 +59,23 @@ definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). apply sym2; apply prop12; apply Eab; - ] - | simplify; intros; whd; split; +qed. + +lemma o_relation_pair_of_relation_pair_morphism : + ∀S,T:category2_of_category1 BP. + unary_morphism2 (arrows2 (category2_of_category1 BP) S T) + (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T)). +intros (S T); + constructor 1; + [ apply (o_relation_pair_of_relation_pair S T); + | apply (o_relation_pair_of_relation_pair_is_morphism S T)] +qed. + +lemma o_relation_pair_of_relation_pair_morphism_respects_id: + ∀o:category2_of_category1 BP. + o_relation_pair_of_relation_pair_morphism o o (id2 (category2_of_category1 BP) o) + = id2 OBP (o_basic_pair_of_basic_pair o). + simplify; intros; whd; split; [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x); @@ -67,8 +83,19 @@ definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). simplify; apply prop12; apply prop22;[2,4,6,8: apply rule #;] - apply (respects_id2 ?? POW (concr o)); - | simplify; intros; whd; split; + apply (respects_id2 ?? POW (concr o)); +qed. + +lemma o_relation_pair_of_relation_pair_morphism_respects_comp: + ∀o1,o2,o3:category2_of_category1 BP. + ∀f1:arrows2 (category2_of_category1 BP) o1 o2. + ∀f2:arrows2 (category2_of_category1 BP) o2 o3. + (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair o1) (o_basic_pair_of_basic_pair o3))) + (o_relation_pair_of_relation_pair_morphism o1 o3 (f2 ∘ f1)) + (comp2 OBP ??? + (o_relation_pair_of_relation_pair_morphism o1 o2 f1) + (o_relation_pair_of_relation_pair_morphism o2 o3 f2)). + simplify; intros; whd; split; [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x); @@ -76,7 +103,15 @@ definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). simplify; apply prop12; apply prop22;[2,4,6,8: apply rule #;] - apply (respects_comp2 ?? POW (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);] + apply (respects_comp2 ?? POW (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c); +qed. + +definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). + constructor 1; + [ apply o_basic_pair_of_basic_pair; + | intros; apply o_relation_pair_of_relation_pair_morphism; + | apply o_relation_pair_of_relation_pair_morphism_respects_id; + | apply o_relation_pair_of_relation_pair_morphism_respects_comp;] qed. theorem BP_to_OBP_faithful: diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 58725373c..3f3389337 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -90,11 +90,11 @@ definition Oid_relation_pair: ∀o:Obasic_pair. Orelation_pair o o. apply (H1 \sup -1);] qed. -definition Orelation_pair_composition: - ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3). - intros; - constructor 1; - [ intros (r r1); +lemma Orelation_pair_composition: + ∀o1,o2,o3:Obasic_pair. + Orelation_pair_setoid o1 o2 → Orelation_pair_setoid o2 o3→Orelation_pair_setoid o1 o3. +intros 3 (o1 o2 o3); + intros (r r1); constructor 1; [ apply (r1 \sub\c ∘ r \sub\c) | apply (r1 \sub\f ∘ r \sub\f) @@ -105,7 +105,16 @@ definition Orelation_pair_composition: apply rule (.= ASSOC ^ -1); apply (.= H‡#); apply rule ASSOC] - | intros; +qed. + + +lemma Orelation_pair_composition_is_morphism: + ∀o1,o2,o3:Obasic_pair. + Πa,a':Orelation_pair_setoid o1 o2.Πb,b':Orelation_pair_setoid o2 o3. + a=a' →b=b' → + Orelation_pair_composition o1 o2 o3 a b + = Orelation_pair_composition o1 o2 o3 a' b'. +intros; change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c)); change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); @@ -116,25 +125,60 @@ definition Orelation_pair_composition: apply (.= e‡#); apply rule (.= ASSOC); apply (.= #‡(Ocommute ?? b')\sup -1); - apply rule (ASSOC \sup -1)] + apply rule (ASSOC \sup -1); qed. - -definition OBP: category2. - constructor 1; - [ apply Obasic_pair - | apply Orelation_pair_setoid - | apply Oid_relation_pair - | apply Orelation_pair_composition - | intros; + +definition Orelation_pair_composition_morphism: + ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3). +intros; constructor 1; +[ apply Orelation_pair_composition; +| apply Orelation_pair_composition_is_morphism;] +qed. + +lemma Orelation_pair_composition_morphism_assoc: +∀o1,o2,o3,o4:Obasic_pair + .Πa12:Orelation_pair_setoid o1 o2 + .Πa23:Orelation_pair_setoid o2 o3 + .Πa34:Orelation_pair_setoid o3 o4 + .Orelation_pair_composition_morphism o1 o3 o4 + (Orelation_pair_composition_morphism o1 o2 o3 a12 a23) a34 + =Orelation_pair_composition_morphism o1 o2 o4 a12 + (Orelation_pair_composition_morphism o2 o3 o4 a23 a34). + intros; change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); apply rule (ASSOC‡#); - | intros; +qed. + +lemma Orelation_pair_composition_morphism_respects_id: +Πo1:Obasic_pair +.Πo2:Obasic_pair + .Πa:Orelation_pair_setoid o1 o2 + .Orelation_pair_composition_morphism o1 o1 o2 (Oid_relation_pair o1) a=a. + intros; change with (⊩ ∘ (a\sub\c ∘ (Oid_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_right2 ????)‡#); - | intros; +qed. + +lemma Orelation_pair_composition_morphism_respects_id_r: +Πo1:Obasic_pair +.Πo2:Obasic_pair + .Πa:Orelation_pair_setoid o1 o2 + .Orelation_pair_composition_morphism o1 o2 o2 a (Oid_relation_pair o2)=a. +intros; change with (⊩ ∘ ((Oid_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); - apply ((id_neutral_left2 ????)‡#);] + apply ((id_neutral_left2 ????)‡#); +qed. + +definition OBP: category2. + constructor 1; + [ apply Obasic_pair + | apply Orelation_pair_setoid + | apply Oid_relation_pair + | apply Orelation_pair_composition_morphism + | apply Orelation_pair_composition_morphism_assoc; + | apply Orelation_pair_composition_morphism_respects_id; + | apply Orelation_pair_composition_morphism_respects_id_r;] qed. definition Obasic_pair_of_objs2_OBP: objs2 OBP → Obasic_pair ≝ λx.x. diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma index b3332c15b..1522dee22 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma @@ -22,41 +22,15 @@ include "o-basic_pairs_to_o-basic_topologies.ma". lemma rOR_full : ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)). exT22 ? (λg:arrows2 rOBP s t. - map_arrows2 ?? OR ?? (ℳ_2 g) = f). -intro; cases s (s_2 s_1 s_eq); clear s; -whd in ⊢ (?→? (? ? (? ?? ? %) ?)→?); -whd in ⊢ (?→?→? ? (λ_:?.? ? ? (? ? ? (? ? ? (? ? ? ? % ?) ?)) ?));; -include "logic/equality.ma". -lapply ( -match s_eq in eq return - (λright_1:?.(λmatched:(eq (objs2 OBP) (map_objs2 (category2_of_category1 BP) OBP BP_to_OBP s_1) right_1). - (∀t:(objs2 rOBP). - (∀f:(carr2 (arrows2 OBTop (map_objs2 OBP OBTop OR right_1) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))). - (exT22 (carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)) - (λg:(carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)). - (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) - (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) - (carr1_OF_Ocontinuous_relation - (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP (*XXX*)right_1 s_1 matched))) - (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) - (fun12 - (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) - (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) - (map_arrows2 OBP OBTop OR right_1 (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) - (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t g))) - ?))))))) - with - [ refl_eq ⇒ ? -]); - STOP. - (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) - (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) - (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (fun12 (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) (map_arrows2 OBP OBTop OR ? (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched) t g))) - (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) f)))))))) with - [ refl_eq ⇒ ? -]); -cases s_eq; clear s_eq s_2; -intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2; + map_arrows2 ?? OR ?? (ℳ_2 g) = f). +intros 2 (s t); cases s (s_2 s_1 s_eq); clear s; +change in match (F2 ??? (mk_Fo ??????)) with s_2; +cases s_eq; clear s_eq s_2; +letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1; +cases t (t_2 t_1 t_eq); clear t; +change in match (F2 ??? (mk_Fo ??????)) with t_2; +cases t_eq; clear t_eq t_2; +letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1; whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?); intro; whd in s_1 t_1; letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1))); @@ -81,7 +55,7 @@ letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1))); | whd; simplify; intros; simplify; whd in ⊢ (? % %); simplify in ⊢ (? % %); lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x))); - [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin; + [ cases Hletin; clear Hletin; lapply (s y); clear s; whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin; whd in Hletin; simplify in Hletin; diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 635e0574c..4387f35b6 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,4 +1,7 @@ 0.5.7 - .../01/2009 - Pàdoa release + * cases tactic speedup in the simplest case of an inductive type + hose right parameters have all to be abstracted when the outtype is + built * maction support added to output notation (adopted for "=" that expands to "= \sub T" to show the equality type) * generation of derived lemmas rewritten to be based on hooks that -- 2.39.2