| 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
|