Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 17:18:33 -0700 (Fri, 17 May 2002)
Revision: 3663
Log message:

      Extend grammar.
      
      1. Now keywords "in" and "IN" are interchangeable.
      So you may write <<'a in 'T>> instead of <<'a IN 'T>>.
      
      2. You may write 'a='b and 'a<>'b for equal{'a;'b} and nequal{'a;'b}
      correspondingly in theories where such terms are defined.
      For example equal{'a;'b} is defined in czf_itt_eq.
      
      Question to Xin and Jason:
      The czf_itt_eq theory defines two terms for equality: eq and equal.
      Which of them do you think will be more usable?
      If eq is more usable, then it is probably better to define 'a='b as eq{'a;'b}.
      
      3. Added some CZF operators to the parser:
      
        'a In 'b
        all x In 'S. 'P['x]
        all x . 'P['x]
        exst x In 'S. 'P['x]
        exst x . 'P['x]
      
      Question (mainly to Xin and Jason): 'a In 'b is probably not the best shortcut for the set theory membership.
      Other possibilities are  sin, ins, in_s, mem, member.
      Do you have any preference?
      
      4. Now all variables may be words or strings. E.g. yo may write <<all "x^2".'P['"x^2"]>>.
      (Previously in some places variables might be strings, in other places they had to be words)
      

Changes	Path
+41 -25	metaprl/filter/base/term_grammar.ml