src/Pure/Isar/proof_context.ML
2001-11-28 ago name space for local thms (export cond_extern, qualified);
2001-11-24 ago type variables: clarified "used" vs. "occ";
2001-11-15 ago fix_frees: rev;
2001-11-11 ago adapted auto_bind_goal, auto_bind_facts;
2001-11-09 ago syntactic declaration of external *and* internal versions of fixes;
2001-11-09 ago theory data: finish method;
2001-11-08 ago proper syntax for structs;
2001-11-07 ago syntax for structures;
2001-11-06 ago cert_def: proper check of args, improved msgs;
2001-11-06 ago local syntax: add_syntax, proper read/pretty functions;
2001-11-06 ago tuned;
2001-11-05 ago added pretty/print functions with context;
2001-11-04 ago added get_thms_with_closure;
2001-11-01 ago fix_frees;
2001-10-31 ago simplified export;
2001-10-24 ago further 1.73 changes: added fix_direct, simplified assume interface;
2001-10-24 ago added read_prop_schematic;
2001-10-23 ago added export_assume, export_presume, export_def (from proof.ML);
2001-10-23 ago print fixed names as plain strings;
2001-10-16 ago simplified exporter interface;
2001-10-16 ago support impromptu terminology of cases parameters;
2001-10-14 ago use ObjectLogic;
2001-08-31 ago Removed tag_assumption.
2001-01-09 ago avoid renaming of params in cases;
2001-01-07 ago tuned output;
2001-01-06 ago apply_case: more robust handling of bounds;
2000-12-04 ago export get_skolem;
2000-11-30 ago schematic props;
2000-11-13 ago added read_terms, read_props (simulataneous type-inference);
2000-11-03 ago fixed two obscurities of "fix": predeclare_terms;
2000-08-29 ago added prems_limit;
2000-08-09 ago thms closure;
2000-08-08 ago norm_hhf results;
2000-08-04 ago dummy_patterns moved to term.ML;
2000-08-03 ago added setmp_verbose;
2000-08-03 ago typ_no_norm;
2000-07-30 ago exporter setup for context elements;
2000-07-13 ago fix(_i): admit internal variables;
2000-07-13 ago "_i" arguments now expected to have skolems already internalized;
2000-07-06 ago tuned msgs;
2000-06-29 ago facts: handle multiple lists of arguments;
2000-06-25 ago added extern_skolem;
2000-05-31 ago get_thm(s): automatic transfer;
2000-05-05 ago GPLed;
2000-03-31 ago tuned;
2000-03-30 ago support Hindley-Milner polymorphisms in binds and facts;
2000-03-15 ago pretty chunks;
2000-03-13 ago cases: preserve order;
2000-03-09 ago check_case: disallow (T)Vars in invoked case;
2000-03-08 ago add_cases: omit unnamed;
2000-03-08 ago handling of local contexts: print_cases, get_case, add_cases;
2000-02-02 ago most_general_varify_tfrees all results;
2000-01-28 ago tuned sig;
2000-01-05 ago TypeInfer.logicT;
1999-10-25 ago improved handling of warn_extra_tfrees;
1999-10-22 ago warn_extra_tfrees (after declare_term);
1999-10-01 ago improved 'fix' / Skolem interfaces;
1999-09-30 ago added cert_skolem;
1999-09-30 ago export def_sort, def_type;
1999-09-25 ago added reset_thms;