<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
2006.09.13  Version 0.04
2006.11.01  Version 0.04.2
2006.12.20  Version 0.10     initial public release

2006.12.20  Version 0.10.1  
- include missing HOL file ottDefine.sml

2006.12.22  Version 0.10.2  
- include missing ottmode.el

2007.01.19  Version 0.10.3   
- bugfixes
- new examples: various TAPL fragments, and an OCaml fragment with
   concurrency (peterson_caml.ott)
- generation of OCaml code for type definitions and generated
   functions (substitution etc)
- merge option to merge ott source files
- improved HOL support infrastructure

2007.01.24  Version 0.10.4
- bugfix: allow "-" in bindspec lexing
  
2007.02.07  Version 0.10.5
- various bugfixes (mostly w.r.t. Coq list support)
- various improvements to examples
- document generation of OCaml code
- (breaking) source syntax changes: keyword "rules" is now replaced by
   "grammar", and hom "caml" is replaced by "ocaml"

2007.04.06  Version 0.10.6
- fixes and additional examples

2007.07.18  Version 0.10.7
- bug fixes

2007.08.13  Version 0.10.8
- rename module Aux to Auxl, to work around a Windows problem

2007.08.28  Version 0.10.9
- add Windows binary-only release

2007.09.04  Version 0.10.10
- new manual, in browsable html, pdf and postscript
- new tex style for typesetting rules (in the tex/ directory)
- move emacs mode and hol auxiliaries into new emacs/ and hol/ directories

2007.09.28  Version 0.10.11
- fix bug in Windows version: properly open files in binary mode when writesys and readsys

2007.10.05  Version 0.10.12
- add missing file from Coq proof support: ott_list_eq_dec.v

2007.10.18  Version 0.10.13
- new (experimental!) switch -picky_multiple_parses <true>,     
   to allow multiple parses if the generated code is
   identical - at present only for filtered LaTeX
- some source documentation
 
2008.02.15  Version 0.10.14
- new parser, with better performance and better support for disambiguation
   (see Section 14 "Parsing Priorities" in the manual, and changes to 
   Section 20 "Reference: The language of symbolic terms")
- new support for context grammars, with automatically generated
   hole-filling functions (see Section 13 "Context rules" in the manual)
- new syntactic sugar flavour of metaproductions: writing "S" instead
   of "M" gives metaproductions that can be used in concrete terms
- various bugfixes

2008.12.16  Version 0.10.15
- support for Isabelle 2008 (Isabelle 2005 syntax no longer produced)
- new option -isabelle_primrec <true> : if set to false then ott
   generates "fun"s instead of "primrec"s  (though Isabelle can only
   sometimes automatically prove termination of these "fun"s).
- new declaration "phantom" to turn off type generation for metavariables.

2009.3.9  Version 0.10.16
- release of the experimental Coq locally-nameless backend
- aesthetic improvements of the Coq output
- -show-post-sort and -show-defns are now <false> by default to make
    output less noisy

2009.7.19 Version 0.10.17

- fix ocamlvar hom bug
- fix bug in Coq backend when dealing with some kinds of dot forms
- suppress printing of number of good/bad definition rules if 
   there are no rules
- change -tex_show_meta false behaviour to not suppress sugar
   productions
- add % at line ends in rules, to prevent extra spaces (per BCP patch)
- remove doc references to the Windows binary distribution.  It should
   be easy to build from source, but we don't have access to a
   suitable machine.


2010.3.24 Version 0.10.18alpha

- The previous command-line options -coq, -hol, etc., are no longer
  supported; they should be replaced by -o. 

- By default (unless -merge true is set) the order of the input file 
  is preserved, so one can have mixed sequences of definitions of
  grammar, of inductive relations, and of embed blocks.

- New command-line options -i <filename> and -o <filename> for
  specifying multiple input and output files.  Input files with
  non-.ott extensions (.v, .thy, .sml, .ml, .tex) are copied verbatim
  into the respective outputs.  The command-line order of these
  options is significant:  the prover output can be split into
  multiple output files; each prover output file specified with -o
  will contain the material from the previous input files specified
  with -i (since the last -o for this prover).

- Better tex default spacing, distinguishing alphabetic and other
  ("symbolic") terminals based on their ott source strings and
  wrapping them in \ottkw{} and \ottsym{} respectively. 

- Support for in-line prover code in premises, e.g.

   {{ prover code mentioning [[x]] and [[\y.z]] }}
   -----------------------------------------------  ::  rulename
   conclusion

- The {{ phantom }} hom can now be applied to metavariables and to
  nonterminal rules.  In both cases it suppresses generation of a prover
  or OCaml definition, but any type homs are taken into account when
  the metavariable or nonterminal root is output as a type. 

- There is a new hom {{ order ... }} that can be applied to
  productions which lets one specify the order of arguments of a
  prover or OCaml constructor independently of the order in which they
  appear in the production.  For example, one might say:

     | e1 e2   :: :: ReversedApp {{ order [[e2]] [[e1]] }}

- There is a new hom {{ coq-universe UniverseName }} that can be
  applied to metavariable or nonterminal rules, eg to force Ott to
  generate definitions in Type instead of in Set. 

- Changed some debug options (eg show-pre-sort)

- Ocaml list homs on productions are now permitted 

- add coq_lngen option for compatibility with the lngen tool

- Bug fixes:
   - problem with comment line in defns terminated with EOF [Jianzhou Zhao]
   - freshness of identifier in Ott generated functions [Jianzhou Zhao]
   - processing of parse tree for some cases of dot forms [Scott Owens]
   - processing of picky_multiple_parses [Scott Owens]
   - added some error checks
   - several fixes in the Coq locally-nameless backend [Stephanie Weirich]
   - performance issue when using contextrules [Nicolas Pouillard]
   - parens in OCaml substitutions for multiple binders [Vilhelm Sjoberg]


2010.03.29 Version 0.20

- The order among mutually recursive nonterminal definitions in
  grammar blocks is now preserved in prover output. 

2010.04.04 Version 0.20.1

- Support coq-universe hom on blocks of definitions, eg:

    defns
    Jop :: '' ::= {{ coq-universe Type }}

     defn
     t1 --> t2 :: ::reduce::'' by


        --------------------------  :: ax_app
        (\x.t1) v2 -->  {v2/x}t1