src/Pure/Isar/proof_context.ML
Tue, 16 Oct 2007 17:06:18 +0200 wenzelm added revert_abbrev;
Mon, 15 Oct 2007 15:29:45 +0200 haftmann swapped constant components
Thu, 11 Oct 2007 19:10:24 +0200 wenzelm replaced Term.equiv_types by Type.similar_types;
Thu, 11 Oct 2007 16:05:30 +0200 wenzelm moved ProofContext.pp to Syntax.pp;
Wed, 10 Oct 2007 17:31:56 +0200 wenzelm generalized notation interface (add or del);
Tue, 09 Oct 2007 00:20:22 +0200 wenzelm generic Syntax.pretty/string_of operations;
Tue, 02 Oct 2007 16:06:41 +0200 wenzelm export tsig_of;
Sun, 30 Sep 2007 16:20:40 +0200 wenzelm add_abbrev: tags (Markup.property list);
Sun, 30 Sep 2007 11:55:14 +0200 wenzelm standard_term_check: include expand_abbrevs (back again);
Sat, 29 Sep 2007 21:39:52 +0200 wenzelm removed redundant const_constraint;
Sat, 29 Sep 2007 08:58:57 +0200 haftmann exported constraint interfaces
Mon, 24 Sep 2007 21:07:38 +0200 wenzelm eliminated ProofContext.read_termTs;
Sun, 23 Sep 2007 23:39:42 +0200 wenzelm removed dead code;
Sun, 23 Sep 2007 23:00:01 +0200 wenzelm made smlnj happy;
Sun, 23 Sep 2007 22:23:35 +0200 wenzelm added read_term_pattern/schematic/abbrev;
Sat, 22 Sep 2007 17:45:57 +0200 wenzelm removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
Mon, 17 Sep 2007 16:36:41 +0200 wenzelm avoid direct access to print_mode;
Sat, 01 Sep 2007 18:17:44 +0200 wenzelm removed unused join_mode;
Sat, 01 Sep 2007 15:47:04 +0200 wenzelm removed obsolete read/cert variations (cf. Syntax.read/check);
Fri, 31 Aug 2007 23:17:25 +0200 wenzelm reject_vars: accept type-inference params;
Fri, 31 Aug 2007 18:46:35 +0200 wenzelm export various inner syntax modes;
Thu, 30 Aug 2007 22:35:40 +0200 wenzelm added join_mode;
Thu, 30 Aug 2007 15:04:48 +0200 wenzelm moved type_mode to type.ML;
Tue, 21 Aug 2007 20:05:38 +0200 wenzelm added inner syntax mode, includes former type_mode and is_stmt;
Mon, 20 Aug 2007 23:41:40 +0200 wenzelm inner syntax: added parse_term/prop;
Mon, 20 Aug 2007 20:44:03 +0200 wenzelm prepare_dummies: NAMED_CRITICAL;
Tue, 14 Aug 2007 23:23:06 +0200 wenzelm added implicit type mode (cf. Type.mode);
Fri, 27 Jul 2007 21:55:22 +0200 wenzelm get_thm etc.: map empty name to dummy_thm;
Mon, 23 Jul 2007 14:06:12 +0200 wenzelm marked some CRITICAL sections (for multithreading);
Wed, 13 Jun 2007 00:02:04 +0200 wenzelm tuned msg;
Sat, 02 Jun 2007 18:05:33 +0200 wenzelm moved specific target/local_abbrev to theory_target.ML;
Tue, 08 May 2007 17:40:22 +0200 wenzelm simplified pretty_thm(_legacy);
Tue, 08 May 2007 15:01:33 +0200 wenzelm legacy_intern_skolem: legacy_feature;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Mon, 23 Apr 2007 20:44:12 +0200 wenzelm sane version of read_termTs (proper freeze);
Sat, 21 Apr 2007 11:07:42 +0200 wenzelm added decode_term (belongs to Syntax module);
Wed, 18 Apr 2007 21:30:14 +0200 wenzelm simplified ProofContext.infer_types(_pats);
Sun, 15 Apr 2007 23:25:55 +0200 wenzelm replaced read_term_legacy by read_prop_legacy;
Sun, 15 Apr 2007 14:32:01 +0200 wenzelm proper interface infer_types(_pat);
Sat, 14 Apr 2007 17:36:05 +0200 wenzelm Term.string_of_vname;
Sat, 14 Apr 2007 00:46:20 +0200 wenzelm added Morphism.transform/form (generic non-sense);
Wed, 04 Apr 2007 00:11:20 +0200 wenzelm renamed Output.has_mode to print_mode_active;
Mon, 26 Feb 2007 20:14:52 +0100 wenzelm added theorems_of;
Fri, 23 Feb 2007 08:39:25 +0100 haftmann add_path for naming in proof contexts
Wed, 13 Dec 2006 15:47:34 +0100 wenzelm target_abbrev: internal mode for abbrevs;
Wed, 13 Dec 2006 14:52:30 +0100 wenzelm local_abbrev: proper fix/declare of local entities;
Tue, 12 Dec 2006 21:25:13 +0100 wenzelm add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
Tue, 12 Dec 2006 20:49:30 +0100 wenzelm notation: Term.equiv_types;
Mon, 11 Dec 2006 21:39:26 +0100 wenzelm advanced translation functions: Proof.context;
Sun, 10 Dec 2006 17:37:55 +0100 wenzelm removed junk;
Sun, 10 Dec 2006 15:30:43 +0100 wenzelm added target_notation/abbrev;
Sat, 09 Dec 2006 18:05:48 +0100 wenzelm added read/pretty_term_abbrev, print_abbrevs;
Thu, 07 Dec 2006 21:08:48 +0100 wenzelm simplified add_abbrev -- single argument;
Thu, 07 Dec 2006 17:58:46 +0100 wenzelm simplified add_abbrevs: no mixfix;
Thu, 07 Dec 2006 00:42:04 +0100 wenzelm reorganized structure Goal vs. Tactic;
Wed, 06 Dec 2006 21:18:58 +0100 wenzelm add_abbrevs: moved common parts to consts.ML;
Tue, 05 Dec 2006 22:14:52 +0100 wenzelm add_notation: permissive about undeclared consts;
Tue, 05 Dec 2006 01:17:32 +0100 wenzelm more careful indexing of local facts;
Tue, 05 Dec 2006 00:29:13 +0100 wenzelm note_thmss: added kind tag and non-official name;
Fri, 01 Dec 2006 17:22:32 +0100 haftmann made SML/NJ happy
less more (0) -300 -100 -60 tip