2 commits

Author	SHA1	Message	Date
Leonardo de Moura	5feef27c2b	feat(frontends/lean/notation_cmd): relax restriction on user defined tokens ... Before this commit, Lean would forbid new tokens containing '(' or ')'. We relax this restriction. Now, we just forbid new tokens starting with '(' or ending with ')'.	2016-01-02 13:58:46 -08:00
Leonardo de Moura	a1006073d4	feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence	2014-10-19 13:39:06 -07:00