Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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 , 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