| Tue, 18 Sep 2007 18:49:17 +0200 |
ballarin |
New function inst_morphism'.
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:15 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
file |
diff |
annotate
|
| Mon, 18 Jun 2007 23:30:46 +0200 |
wenzelm |
tuned conjunction tactics: slightly smaller proof terms;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:51 +0200 |
wenzelm |
Method.Basic: include position;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:47 +0200 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 00:46:22 +0200 |
wenzelm |
inst(T)_morphism: avoid reference to static theory value;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 10:01:43 +0200 |
ballarin |
Experimental interpretation code for definitions.
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:05 +0100 |
wenzelm |
pretty_statement: more careful handling of name_hint;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:14 +0100 |
wenzelm |
added facts_map;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:22 +0100 |
wenzelm |
added map_ctxt_attrib;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:17 +0100 |
wenzelm |
simultaneous fact morphism;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:36 +0100 |
wenzelm |
Morphism.thm_morphism;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:52:15 +0100 |
wenzelm |
added morph_ctxt, morph_witness;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:37 +0100 |
wenzelm |
notes: proper kind;
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:51 +0200 |
wenzelm |
Attrib.pretty_attrib;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:14 +0200 |
wenzelm |
replaced generalize_facts by full export_(standard_)facts;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:58 +0200 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:57 +0200 |
wenzelm |
added generalize_facts;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:11 +0200 |
wenzelm |
Assumption.assume;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2006 20:01:46 +0200 |
wenzelm |
print_statement: tuned Variable operations;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 11:17:09 +0200 |
ballarin |
New function transfer_witness lifting Thm.transfer to witnesses.
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:46 +0200 |
wenzelm |
prove_witness: context;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:58 +0200 |
wenzelm |
instantiate_tfrees: Thm.generalize;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 23:08:54 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:23 +0200 |
wenzelm |
added satisfy_ctxt;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:31 +0200 |
wenzelm |
added facts_of;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:23 +0200 |
wenzelm |
added params_of, prems_of;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:05 +0200 |
wenzelm |
pretty: do not exterm thm names;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 25 Apr 2006 22:23:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:36 +0100 |
wenzelm |
added pretty_statement;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 16:29:36 +0100 |
wenzelm |
added pretty_stmt;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:31:34 +0100 |
wenzelm |
always use Attrib.src;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 12:52:19 +0100 |
wenzelm |
added concluding statements: Shows/Obtains;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:08 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:31 +0100 |
wenzelm |
pretty_locale: backquote notes;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:55 +0100 |
wenzelm |
Explicit data structures for some Isar language elements.
|
file |
diff |
annotate
|