src/Pure/Isar/element.ML
Mon, 10 Nov 2008 19:42:21 +0100 haftmann more verbose element printing
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:29 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Fri, 18 Apr 2008 23:49:44 +0200 wenzelm tuned;
Thu, 17 Apr 2008 22:22:28 +0200 wenzelm print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
Sat, 12 Apr 2008 17:00:40 +0200 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Fri, 21 Dec 2007 16:18:23 +0100 ballarin Fixed eta constraction issue in compose_witness
Fri, 14 Dec 2007 17:56:08 +0100 wenzelm added close_witness;
Mon, 05 Nov 2007 23:17:03 +0100 wenzelm tuned satisfy_thm;
Mon, 05 Nov 2007 17:48:34 +0100 ballarin Removed inst_morphism'; satisfy_thm avoids compose.
Fri, 26 Oct 2007 17:18:32 +0200 wenzelm proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Tue, 18 Sep 2007 18:49:17 +0200 ballarin New function inst_morphism'.
Fri, 03 Aug 2007 16:28:15 +0200 wenzelm replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
Mon, 18 Jun 2007 23:30:46 +0200 wenzelm tuned conjunction tactics: slightly smaller proof terms;
Wed, 13 Jun 2007 00:01:51 +0200 wenzelm Method.Basic: include position;
Thu, 10 May 2007 00:39:45 +0200 wenzelm moved conversions to structure Conv;
Sun, 15 Apr 2007 14:31:47 +0200 wenzelm Thm.fold_terms;
Sat, 14 Apr 2007 00:46:22 +0200 wenzelm inst(T)_morphism: avoid reference to static theory value;
Fri, 13 Apr 2007 10:01:43 +0200 ballarin Experimental interpretation code for definitions.
Tue, 03 Apr 2007 19:24:13 +0200 wenzelm renamed Variable.import to import_thms (avoid clash with Alice keywords);
Sat, 30 Dec 2006 16:08:05 +0100 wenzelm pretty_statement: more careful handling of name_hint;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Thu, 30 Nov 2006 14:17:29 +0100 wenzelm qualified MetaSimplifier.norm_hhf(_protect);
Wed, 29 Nov 2006 04:11:14 +0100 wenzelm added facts_map;
Sun, 26 Nov 2006 18:07:22 +0100 wenzelm added map_ctxt_attrib;
Fri, 24 Nov 2006 22:05:17 +0100 wenzelm simultaneous fact morphism;
Thu, 23 Nov 2006 20:33:36 +0100 wenzelm Morphism.thm_morphism;
Thu, 23 Nov 2006 00:52:15 +0100 wenzelm added morph_ctxt, morph_witness;
Tue, 21 Nov 2006 18:07:37 +0100 wenzelm notes: proper kind;
Sat, 14 Oct 2006 23:25:51 +0200 wenzelm Attrib.pretty_attrib;
Sat, 07 Oct 2006 01:31:14 +0200 wenzelm replaced generalize_facts by full export_(standard_)facts;
Fri, 15 Sep 2006 22:56:13 +0200 wenzelm renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
Wed, 02 Aug 2006 22:26:58 +0200 wenzelm removed obsolete Drule.frees/vars_of etc.;
Sun, 30 Jul 2006 21:28:57 +0200 wenzelm added generalize_facts;
Thu, 27 Jul 2006 13:43:11 +0200 wenzelm Assumption.assume;
Wed, 26 Jul 2006 19:37:41 +0200 wenzelm Variable.import(T): result includes fixed types/terms;
Tue, 18 Jul 2006 20:01:46 +0200 wenzelm print_statement: tuned Variable operations;
Tue, 11 Jul 2006 11:17:09 +0200 ballarin New function transfer_witness lifting Thm.transfer to witnesses.
Sat, 08 Jul 2006 12:54:46 +0200 wenzelm prove_witness: context;
Tue, 04 Jul 2006 19:49:58 +0200 wenzelm instantiate_tfrees: Thm.generalize;
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation.
Thu, 15 Jun 2006 23:08:54 +0200 wenzelm ProofContext: moved variable operations to struct Variable;
Mon, 12 Jun 2006 21:19:06 +0200 wenzelm tuned;
Sun, 11 Jun 2006 21:59:23 +0200 wenzelm added satisfy_ctxt;
Wed, 07 Jun 2006 02:01:31 +0200 wenzelm added facts_of;
Mon, 05 Jun 2006 21:54:23 +0200 wenzelm added params_of, prems_of;
Fri, 26 May 2006 22:20:05 +0200 wenzelm pretty: do not exterm thm names;
Sun, 07 May 2006 00:22:05 +0200 wenzelm removed 'concl is' patterns;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Tue, 25 Apr 2006 22:23:41 +0200 wenzelm tuned;
Tue, 21 Mar 2006 12:18:15 +0100 wenzelm avoid polymorphic equality;
Tue, 14 Mar 2006 22:06:36 +0100 wenzelm added pretty_statement;
Tue, 14 Mar 2006 16:29:36 +0100 wenzelm added pretty_stmt;
Thu, 02 Feb 2006 16:31:34 +0100 wenzelm always use Attrib.src;
Thu, 02 Feb 2006 12:52:19 +0100 wenzelm added concluding statements: Shows/Obtains;
Fri, 13 Jan 2006 01:13:08 +0100 wenzelm uniform handling of fixes;
Sat, 07 Jan 2006 12:26:31 +0100 wenzelm pretty_locale: backquote notes;
less more (0) tip