Wed, 18 Jun 2008 22:32:02 +0200 improved error output -- variant/mark bounds;
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;
Wed, 18 Jun 2008 22:32:01 +0200 load type_infer.ML after Syntax module;
wenzelm [Wed, 18 Jun 2008 22:32:01 +0200] rev 27262
load type_infer.ML after Syntax module;
Wed, 18 Jun 2008 18:55:10 +0200 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm [Wed, 18 Jun 2008 18:55:10 +0200] rev 27261
eliminated old Sign.read_term/Thm.read_cterm etc.;
Wed, 18 Jun 2008 18:55:08 +0200 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
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);
Wed, 18 Jun 2008 18:55:07 +0200 export transfer_syntax;
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;
Wed, 18 Jun 2008 18:55:06 +0200 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;
Wed, 18 Jun 2008 18:55:05 +0200 removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
wenzelm [Wed, 18 Jun 2008 18:55:05 +0200] rev 27257
removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
Wed, 18 Jun 2008 18:55:04 +0200 added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
wenzelm [Wed, 18 Jun 2008 18:55:04 +0200] rev 27256
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
Wed, 18 Jun 2008 18:55:03 +0200 removed obsolete read_def_cterms/read_cterm;
wenzelm [Wed, 18 Jun 2008 18:55:03 +0200] rev 27255
removed obsolete read_def_cterms/read_cterm;
Wed, 18 Jun 2008 18:55:02 +0200 load proof term operations later;
wenzelm [Wed, 18 Jun 2008 18:55:02 +0200] rev 27254
load proof term operations later;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip