updated

renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;

added implicit type mode (cf. Type.mode); added inner syntax parsers for sort/typ (no term/prop yet); infer_types: exception TYPE => error; read_vars: Syntax.parse_typ;

Syntax.global_read_sort;

infer_types: depend on Type.mode;

type mode: models certification mode (default, syntax, abbrev); replaced certify_typ_syntax/abbrev by certify_typ_mode;

replaced certify_typ_syntax/abbrev by certify_typ_mode; removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';

tuned order;

avoid low-level tsig;

fixed dummyT (used as constraint);

remove redundant assumption from Rep_range lemma

minimize imports

rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]

extended linear arith capabilities with code by Amine

fix the generation of eqvt lemma of equality form from the imp form when the relation is equality

moved Tools/xml.ML to General/xml.ML (again);

added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;

tuned;

PrimitiveDefs.dest/abs_def;

PrimitiveDefs.dest_def; Syntax.standard_read;

Primitive definition forms.

moved support for primitive defs to primitive_defs.ML;

use logic.ML earlier; added primitive_defs.ML;

moved Tools/xml.ML to General/xml.ML (again); added primitive_defs.ML;

PrimitiveDefs.mk_defpair;

be a bit more ressource cautious with multi-threading (-M 20 instead of 99)

fixed syntax

simplified

fixed OCaml bug

*** empty log message ***