From 43d3607afd27248d8df1bca20908307330a3871a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 8 Feb 2006 15:35:08 +0000 Subject: [PATCH] comment out an incomplete proof --- helm/software/matita/library/algebra/groups.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index ed1caebe3..970a5e388 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -244,6 +244,7 @@ for @{ 'disjoint $a $b }. interpretation "Left cosets disjoint" 'disjoint C C' = (cic:/matita/algebra/groups/left_coset_disjoint.con _ C C'). +(* (* The following should be a one-shot alias! *) alias symbol "belongs_to" (instance 0) = "Belongs to subgroup". theorem foo: @@ -267,6 +268,7 @@ exists; | ]. qed. +*) (*theorem foo: \forall G:Group. \forall x1,x2:G. \forall H:subgroup G. @@ -304,4 +306,4 @@ definition left_coset_eq ≝ (element ? H)·(embed ? ? (subgroup_is_subgroup ? H) ˜ x) = (element ? H')·(embed ? ? (subgroup_is_subgroup ? H') ˜ y)). *) -*) \ No newline at end of file +*) -- 2.39.5