wenzelm [Wed, 18 Jun 2008 22:32:04 +0200] rev 27265
TypeExt.type_constraint;
wenzelm [Wed, 18 Jun 2008 22:32:03 +0200] rev 27264
simplified TypeInfer.infer_types;
wenzelm [Wed, 18 Jun 2008 22:32:02 +0200] rev 27263
improved error output -- variant/mark bounds;
simplified infer_types -- always freeze, no result substitution;
wenzelm [Wed, 18 Jun 2008 22:32:01 +0200] rev 27262
load type_infer.ML after Syntax module;
wenzelm [Wed, 18 Jun 2008 18:55:10 +0200] rev 27261
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm [Wed, 18 Jun 2008 18:55:08 +0200] rev 27260
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
read_term: imitate old behaviour (allow_dummies, mode_schematic);
wenzelm [Wed, 18 Jun 2008 18:55:07 +0200] rev 27259
export transfer_syntax;
added allow_dummies feature (for legacy emulations);
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm [Wed, 18 Jun 2008 18:55:06 +0200] rev 27258
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;