X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCGroups.ma;h=67d508c12fff8abca315b2a9aa0747e26de34b33;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=42287b0e27d2f38bc110a47977fa82a3bd7e59ae;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma index 42287b0e2..67d508c12 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *) @@ -47,7 +47,7 @@ inline "cic:/CoRN/algebra/CGroups/is_CGroup.con". inline "cic:/CoRN/algebra/CGroups/CGroup.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con 0 (* compounds *). (* End_SpecReals *) @@ -57,6 +57,10 @@ coercion "cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con" 0 (* compounds *). Implicit Arguments cg_inv [c]. *) +(* NOTATION +Notation "[--] x" := (cg_inv x) (at level 2, right associativity). +*) + inline "cic:/CoRN/algebra/CGroups/cg_minus.con". (*#* @@ -70,6 +74,10 @@ and [ [-] ] with [minus]. Implicit Arguments cg_minus [G]. *) +(* NOTATION +Infix "[-]" := cg_minus (at level 50, left associativity). +*) + (* End_SpecReals *) (*#* @@ -79,15 +87,15 @@ Implicit Arguments cg_minus [G]. *) (* UNEXPORTED -Section CGroup_axioms. +Section CGroup_axioms *) -inline "cic:/CoRN/algebra/CGroups/G.var". +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_axioms/G.var". inline "cic:/CoRN/algebra/CGroups/cg_inverse.con". (* UNEXPORTED -End CGroup_axioms. +End CGroup_axioms *) (*#* @@ -98,10 +106,10 @@ General properties of groups. *) (* UNEXPORTED -Section CGroup_basics. +Section CGroup_basics *) -inline "cic:/CoRN/algebra/CGroups/G.var". +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_basics/G.var". inline "cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con". @@ -180,31 +188,31 @@ inline "cic:/CoRN/algebra/CGroups/x_minus_x.con". *) (* UNEXPORTED -Section SubCGroups. +Section SubCGroups *) -inline "cic:/CoRN/algebra/CGroups/P.var". +alias id "P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/P.var". -inline "cic:/CoRN/algebra/CGroups/Punit.var". +alias id "Punit" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/Punit.var". -inline "cic:/CoRN/algebra/CGroups/op_pres_P.var". +alias id "op_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/op_pres_P.var". -inline "cic:/CoRN/algebra/CGroups/inv_pres_P.var". +alias id "inv_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/inv_pres_P.var". -inline "cic:/CoRN/algebra/CGroups/subcrr.con". +inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subcrr.con" "CGroup_basics__SubCGroups__". -inline "cic:/CoRN/algebra/CGroups/subinv.con". +inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subinv.con" "CGroup_basics__SubCGroups__". inline "cic:/CoRN/algebra/CGroups/isgrp_scrr.con". inline "cic:/CoRN/algebra/CGroups/Build_SubCGroup.con". (* UNEXPORTED -End SubCGroups. +End SubCGroups *) (* UNEXPORTED -End CGroup_basics. +End CGroup_basics *) (* UNEXPORTED @@ -230,10 +238,10 @@ Hint Resolve cg_minus_wd: algebra_c. *) (* UNEXPORTED -Section Assoc_properties. +Section Assoc_properties *) -inline "cic:/CoRN/algebra/CGroups/G.var". +alias id "G" = "cic:/CoRN/algebra/CGroups/Assoc_properties/G.var". inline "cic:/CoRN/algebra/CGroups/assoc_2.con". @@ -244,7 +252,7 @@ inline "cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con". inline "cic:/CoRN/algebra/CGroups/plus_resp_eq.con". (* UNEXPORTED -End Assoc_properties. +End Assoc_properties *) (* UNEXPORTED @@ -260,10 +268,10 @@ Specific properties of apartness. *) (* UNEXPORTED -Section cgroups_apartness. +Section cgroups_apartness *) -inline "cic:/CoRN/algebra/CGroups/G.var". +alias id "G" = "cic:/CoRN/algebra/CGroups/cgroups_apartness/G.var". inline "cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con". @@ -288,7 +296,7 @@ inline "cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con". inline "cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con". (* UNEXPORTED -End cgroups_apartness. +End cgroups_apartness *) (* UNEXPORTED @@ -300,7 +308,7 @@ Hint Resolve minus_ap_zero zero_minus_apart inv_resp_ap_zero: algebra. *) (* UNEXPORTED -Section CGroup_Ops. +Section CGroup_Ops *) (*#* @@ -314,22 +322,22 @@ by [P] and [Q]. %\end{convention}% *) -inline "cic:/CoRN/algebra/CGroups/G.var". +alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/G.var". -inline "cic:/CoRN/algebra/CGroups/F.var". +alias id "F" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F.var". -inline "cic:/CoRN/algebra/CGroups/F'.var". +alias id "F'" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F'.var". (* begin hide *) -inline "cic:/CoRN/algebra/CGroups/P.con". +inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/P.con" "CGroup_Ops__". -inline "cic:/CoRN/algebra/CGroups/Q.con". +inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/Q.con" "CGroup_Ops__". (* end hide *) (* UNEXPORTED -Section Part_Function_Inv. +Section Part_Function_Inv *) inline "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con". @@ -337,11 +345,11 @@ inline "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con". inline "cic:/CoRN/algebra/CGroups/Finv.con". (* UNEXPORTED -End Part_Function_Inv. +End Part_Function_Inv *) (* UNEXPORTED -Section Part_Function_Minus. +Section Part_Function_Minus *) inline "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con". @@ -349,7 +357,7 @@ inline "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con". inline "cic:/CoRN/algebra/CGroups/Fminus.con". (* UNEXPORTED -End Part_Function_Minus. +End Part_Function_Minus *) (*#* @@ -357,7 +365,7 @@ End Part_Function_Minus. %\end{convention}% *) -inline "cic:/CoRN/algebra/CGroups/R.var". +alias id "R" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/R.var". inline "cic:/CoRN/algebra/CGroups/included_FInv.con". @@ -370,17 +378,25 @@ inline "cic:/CoRN/algebra/CGroups/included_FMinus'.con". inline "cic:/CoRN/algebra/CGroups/included_FMinus''.con". (* UNEXPORTED -End CGroup_Ops. +End CGroup_Ops *) (* UNEXPORTED Implicit Arguments Finv [G]. *) +(* NOTATION +Notation "{--} x" := (Finv x) (at level 2, right associativity). +*) + (* UNEXPORTED Implicit Arguments Fminus [G]. *) +(* NOTATION +Infix "{-}" := Fminus (at level 50, left associativity). +*) + (* UNEXPORTED Hint Resolve included_FInv included_FMinus : included. *)