src/Pure/Isar/proof_context.ML
Fri, 14 Nov 2003 14:35:55 +0100 ballarin Type inference bug in Isar attributes "where" and "of" fixed.
Fri, 29 Aug 2003 15:19:02 +0200 ballarin Methods rule_tac etc support static (Isar) contexts.
Mon, 07 Oct 2002 19:01:51 +0200 nipkow take/drop -> splitAt
Tue, 27 Aug 2002 17:25:44 +0200 wenzelm thms_containing: allow "_" in specification;
Tue, 06 Aug 2002 11:20:47 +0200 wenzelm fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);
Mon, 29 Jul 2002 21:39:22 +0200 wenzelm tuned messages;
Sat, 27 Jul 2002 21:55:14 +0200 wenzelm make SML/NJ happy;
Fri, 26 Jul 2002 21:09:39 +0200 wenzelm support for split assumptions in cases (hyps vs. prems);
Wed, 24 Jul 2002 00:12:50 +0200 wenzelm tuned view;
Fri, 19 Jul 2002 18:44:07 +0200 wenzelm support locale ``views'' (for cumulative predicates);
Tue, 16 Jul 2002 18:42:07 +0200 wenzelm export_standard supercedes export_single;
Tue, 02 Jul 2002 17:44:13 +0200 wenzelm thms_containing: optional limit argument;
Tue, 02 Jul 2002 16:59:52 +0200 wenzelm tuned print_thms_containing;
Tue, 02 Jul 2002 15:44:04 +0200 wenzelm print_thms_containing: index variables, refer to local facts as well;
Wed, 30 Jan 2002 14:00:25 +0100 wenzelm prep_mixfix': proper use of Syntax.literal;
Tue, 22 Jan 2002 21:19:15 +0100 wenzelm qualified_result replaces qualified;
Thu, 17 Jan 2002 21:04:36 +0100 wenzelm Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
Tue, 15 Jan 2002 21:09:01 +0100 wenzelm removed second copy of show_hyps;
Fri, 11 Jan 2002 00:29:54 +0100 wenzelm have_thmss vs. have_thmss_i;
Thu, 10 Jan 2002 16:09:26 +0100 wenzelm export_single;
Fri, 21 Dec 2001 00:40:52 +0100 wenzelm added add_fixes: derives mssing type scheme from mixfix;
Wed, 19 Dec 2001 00:30:13 +0100 wenzelm generalize type variables properly: start with occurrences in objects
Tue, 18 Dec 2001 02:20:02 +0100 wenzelm tuned Type.unify;
Fri, 14 Dec 2001 11:57:03 +0100 wenzelm export used_types;
Thu, 06 Dec 2001 22:38:50 +0100 wenzelm added default_type;
Wed, 28 Nov 2001 00:43:50 +0100 wenzelm name space for local thms (export cond_extern, qualified);
Sat, 24 Nov 2001 17:00:35 +0100 wenzelm type variables: clarified "used" vs. "occ";
Thu, 15 Nov 2001 18:36:24 +0100 wenzelm fix_frees: rev;
Sun, 11 Nov 2001 21:37:20 +0100 wenzelm adapted auto_bind_goal, auto_bind_facts;
Fri, 09 Nov 2001 22:52:38 +0100 wenzelm syntactic declaration of external *and* internal versions of fixes;
Fri, 09 Nov 2001 00:19:20 +0100 wenzelm theory data: finish method;
Thu, 08 Nov 2001 00:26:41 +0100 wenzelm proper syntax for structs;
Wed, 07 Nov 2001 18:18:19 +0100 wenzelm syntax for structures;
Tue, 06 Nov 2001 23:56:14 +0100 wenzelm cert_def: proper check of args, improved msgs;
Tue, 06 Nov 2001 19:29:06 +0100 wenzelm local syntax: add_syntax, proper read/pretty functions;
Tue, 06 Nov 2001 01:21:10 +0100 wenzelm tuned;
Mon, 05 Nov 2001 21:01:59 +0100 wenzelm added pretty/print functions with context;
Sun, 04 Nov 2001 21:00:06 +0100 wenzelm added get_thms_with_closure;
Thu, 01 Nov 2001 21:11:52 +0100 wenzelm fix_frees;
Wed, 31 Oct 2001 22:02:11 +0100 wenzelm simplified export;
Wed, 24 Oct 2001 19:20:02 +0200 wenzelm further 1.73 changes: added fix_direct, simplified assume interface;
Wed, 24 Oct 2001 19:18:23 +0200 wenzelm added read_prop_schematic;
Tue, 23 Oct 2001 23:29:29 +0200 wenzelm added export_assume, export_presume, export_def (from proof.ML);
Tue, 23 Oct 2001 22:59:14 +0200 wenzelm print fixed names as plain strings;
Tue, 16 Oct 2001 23:02:14 +0200 wenzelm simplified exporter interface;
Tue, 16 Oct 2001 00:34:34 +0200 wenzelm support impromptu terminology of cases parameters;
Sun, 14 Oct 2001 20:09:19 +0200 wenzelm use ObjectLogic;
Fri, 31 Aug 2001 16:22:02 +0200 berghofe Removed tag_assumption.
Tue, 09 Jan 2001 15:17:08 +0100 wenzelm avoid renaming of params in cases;
Sun, 07 Jan 2001 21:36:59 +0100 wenzelm tuned output;
Sat, 06 Jan 2001 21:31:09 +0100 wenzelm apply_case: more robust handling of bounds;
Mon, 04 Dec 2000 23:18:24 +0100 wenzelm export get_skolem;
Thu, 30 Nov 2000 20:07:35 +0100 wenzelm schematic props;
Mon, 13 Nov 2000 22:05:57 +0100 wenzelm added read_terms, read_props (simulataneous type-inference);
Fri, 03 Nov 2000 21:28:15 +0100 wenzelm fixed two obscurities of "fix": predeclare_terms;
Tue, 29 Aug 2000 20:14:42 +0200 wenzelm added prems_limit;
Wed, 09 Aug 2000 21:02:45 +0200 wenzelm thms closure;
Tue, 08 Aug 2000 01:17:59 +0200 wenzelm norm_hhf results;
Fri, 04 Aug 2000 23:02:11 +0200 wenzelm dummy_patterns moved to term.ML;
Thu, 03 Aug 2000 18:45:15 +0200 wenzelm added setmp_verbose;
less more (0) -100 -60 tip