Removing of Extended ASCII from the JFM

Propositions of changes

Symbol	change to
ZF_MODEL
pred D,f H means	|=
pred E H means	|=
QMAX_1
pred p q means	|-
pred p q means	<==>
EQUATION
pred A e means	|=
pred A E means	|=
CQC_THE3
pred p q means	|-
pred X Y means	|-
pred X means	|-
pred X Y means	|-|
pred p q means	|-|
pred p q means	<==>
CQC_THE1
pred Xs means	|-
VALUAT_1
pred J,v p means	|=
pred J p means	|=
ZFREFLE1
pred M F means	|=
pred M1 M2 means	<==>
DECOMP_1
pred f is_-continuous means	is_alpha-continuous
pred f is_(c,)-continuous means	is_(c,alpha)-continuous
pred f is_(,p)-continuous means	is_(alpha,p)-continuous
pred f is_(,s)-continuous means	is_(alpha,s)-continuous
pred f is_(,ps)-continuous means	is_(alpha,ps)-continuous
REWRITE1
pred a,b are_convergent1_wrt R means	are_convergent<=1_wrt
pred a,b are_divergent1_wrt R means	are_divergent<=1_wrt
JORDAN4
pred g is_a_part_of f,i1,i2 means	is_a_part>_of
pred g is_a_part_of f,i1,i2 means	is_a_part>_of
PRELAMB
pred f > x means	===>
pred x <> y means	<===>
LATTICE3
pred a is__than X means	is_<=_than
pred X is__than a means	is_<=_than

DECOMP_1
func Int B -> Subset of T equals	alphaInt
func T^ -> Subset-Family of T equals	T^alpha
func D(c,)(T) -> Subset-Family of T equals	D(c,alpha)
func D(,p)(T) -> Subset-Family of T equals	D(alpha,p)
func D(,s)(T) -> Subset-Family of T equals	D(alpha,s)
func D(,ps)(T) -> Subset-Family of T equals	D(alpha,ps)
ENS_1
func Dom V -> Function of Maps V,V means	fDom
func Cod V -> Function of Maps V,V means	fCod
func Comp V -> PartFunc of [:Maps V,Maps V:],Maps V means	fComp
func Id V -> Function of V,Maps V means	fId
COH_SP
func Dom X -> Function of MapsT(X),TOL(X) means	fDom
func Cod X -> Function of MapsT(X),TOL(X) means	fCod
func Comp X -> PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) means	fComp
func Id X -> Function of TOL(X),MapsT(X) means	fId
ZF_COLLA
func M (E,A) -> set means	M_mi
MEASURE7
func L_FIELD -> sigma_Field_Subset of REAL equals	Lmi_sigmaFIELD
func L -> sigma_Measure of L_FIELD equals	L_mi
METRIC_1
func Empty-to-zero -> Function of [:{},{}:], REAL equals	Empty2-to-zero
TOPREAL1
func R-unit_square -> Subset of TOP-REAL 2 equals	R2-unit-square
SUPINF_1
func + -> set equals	+infty
func - -> set equals	-infty
METRIC_2
func x -> Subset of M equals	x-neighbour
func M -> set equals	M-neighbour
func dist M -> Function of [:M,M:],REAL means	nbourdist
FIN_TOPO
func A^ -> Subset of the carrier of FT equals	A^delta
func A^i -> Subset of the carrier of FT equals	A^deltai
func A^o -> Subset of the carrier of FT equals	A^deltao
MIDSP_2
func 2x -> Element of the carrier of G equals	Double x
func x -> Element of the carrier of G means	Half x
GRCAT_1
func GroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals	MidOpGroupObjects
func GroupCat(UN) -> Subcategory of AbGroupCat(UN) equals	MidOpGroupCat
EUCLID
func [ x,y ] -> Point of TOP-REAL 2 equals	|[ r ]|
JORDAN2B
func [ r ] -> Point of TOP-REAL 1 equals	|[ r ]|
CLOSURE2
func : S : -> ManySortedSet of I equals	|: S :|
SYMSP_1
func (a,b,x) -> Element of the carrier of F means	ProJ
func (a,b,x,y) -> Element of the carrier of F means	PProJ
ORTSP_1
func (a,b,x) -> Element of the carrier of F means	ProJ
func (a,b,x,y) -> Element of the carrier of F means	PProJ
ANALTRAP
func (w,y,u,v) -> Real equals	PProJ
PROJRED1
func J(K,p,L) -> PartFunc of the Points of IPP,the Points of IPP means	IncProj
REARRAN1
func (F,A) -> PartFunc of C,REAL equals	land
func (F,A) -> PartFunc of C,REAL equals	lor

SYNONYMS: