Re: [isabelle] Reconciling FinFuns in Distro and AFP



On 09/09/16 12:22, Tobias Nipkow wrote:
> 
> Potentially also restrict_map, although that is a natural operation.
> [It's math syntax would ideally use the symbol \upharpponright, but that
> does not exist yet.]

That symbol is called \<restriction> in $ISABELLE_HOME/etc/symbols. It
is used in theory Map for restrict_map latex syntax only.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.