src/Pure/Isar/proof_context.ML
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type variables.
2003-11-14 ballarin 2003-11-14 Type inference bug in Isar attributes "where" and "of" fixed.
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2002-08-27 wenzelm 2002-08-27 thms_containing: allow "_" in specification;
2002-08-06 wenzelm 2002-08-06 fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);
2002-07-29 wenzelm 2002-07-29 tuned messages;
2002-07-27 wenzelm 2002-07-27 make SML/NJ happy;
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-24 wenzelm 2002-07-24 tuned view;
2002-07-19 wenzelm 2002-07-19 support locale ``views'' (for cumulative predicates);
2002-07-16 wenzelm 2002-07-16 export_standard supercedes export_single;
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 tuned print_thms_containing;
2002-07-02 wenzelm 2002-07-02 print_thms_containing: index variables, refer to local facts as well;
2002-01-30 wenzelm 2002-01-30 prep_mixfix': proper use of Syntax.literal;
2002-01-22 wenzelm 2002-01-22 qualified_result replaces qualified;
2002-01-17 wenzelm 2002-01-17 Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
2002-01-15 wenzelm 2002-01-15 removed second copy of show_hyps;
2002-01-11 wenzelm 2002-01-11 have_thmss vs. have_thmss_i;
2002-01-10 wenzelm 2002-01-10 export_single;
2001-12-21 wenzelm 2001-12-21 added add_fixes: derives mssing type scheme from mixfix;
2001-12-19 wenzelm 2001-12-19 generalize type variables properly: start with occurrences in objects rather than the inner context! tuned interface of generalize;
2001-12-18 wenzelm 2001-12-18 tuned Type.unify; do *not* declare TVar names as used;
2001-12-14 wenzelm 2001-12-14 export used_types; tuned;
2001-12-06 wenzelm 2001-12-06 added default_type;
2001-11-28 wenzelm 2001-11-28 name space for local thms (export cond_extern, qualified); improved internal naming of fixes;
2001-11-24 wenzelm 2001-11-24 type variables: clarified "used" vs. "occ";
2001-11-15 wenzelm 2001-11-15 fix_frees: rev;
2001-11-11 wenzelm 2001-11-11 adapted auto_bind_goal, auto_bind_facts;
2001-11-09 wenzelm 2001-11-09 syntactic declaration of external *and* internal versions of fixes; tuned warn_extra_tfrees;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-11-08 wenzelm 2001-11-08 proper syntax for structs;
2001-11-07 wenzelm 2001-11-07 syntax for structures;
2001-11-06 wenzelm 2001-11-06 cert_def: proper check of args, improved msgs; tuned;
2001-11-06 wenzelm 2001-11-06 local syntax: add_syntax, proper read/pretty functions;
2001-11-06 wenzelm 2001-11-06 tuned;
2001-11-05 wenzelm 2001-11-05 added pretty/print functions with context; added cert_def; print_asms covers both fixes and assumes;
2001-11-04 wenzelm 2001-11-04 added get_thms_with_closure; fix_frees: only new ones;
2001-11-01 wenzelm 2001-11-01 fix_frees; improved export_def: handle args on lhs;
2001-10-31 wenzelm 2001-10-31 simplified export; tuned printing of fixes;
2001-10-24 wenzelm 2001-10-24 further 1.73 changes: added fix_direct, simplified assume interface;
2001-10-24 wenzelm 2001-10-24 added read_prop_schematic;
2001-10-23 wenzelm 2001-10-23 added export_assume, export_presume, export_def (from proof.ML);
2001-10-23 wenzelm 2001-10-23 print fixed names as plain strings;
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-14 wenzelm 2001-10-14 use ObjectLogic;
2001-08-31 berghofe 2001-08-31 Removed tag_assumption.
2001-01-09 wenzelm 2001-01-09 avoid renaming of params in cases;
2001-01-07 wenzelm 2001-01-07 tuned output;
2001-01-06 wenzelm 2001-01-06 apply_case: more robust handling of bounds; moved norm_hhf to Pure/tactic.ML;
2000-12-04 wenzelm 2000-12-04 export get_skolem;
2000-11-30 wenzelm 2000-11-30 schematic props;
2000-11-13 wenzelm 2000-11-13 added read_terms, read_props (simulataneous type-inference);
2000-11-03 wenzelm 2000-11-03 fixed two obscurities of "fix": predeclare_terms;
2000-08-29 wenzelm 2000-08-29 added prems_limit;
2000-08-09 wenzelm 2000-08-09 thms closure;
2000-08-08 wenzelm 2000-08-08 norm_hhf results;