| Tue, 16 Dec 2008 20:18:46 +0100 |
ballarin |
Transfer morphism with theory closure.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 12:08:10 +0100 |
ballarin |
Use correct mode when parsing elements and conclusion.
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 25 Nov 2008 18:07:33 +0100 |
ballarin |
Use standard export function.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
| Wed, 19 Nov 2008 17:00:00 +0100 |
ballarin |
Basic types not qualified.
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:07 +0100 |
haftmann |
diagnostic output for name bindings
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 19:42:21 +0100 |
haftmann |
more verbose element printing
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:29 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Fri, 18 Apr 2008 23:49:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:28 +0200 |
wenzelm |
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:40 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Fri, 21 Dec 2007 16:18:23 +0100 |
ballarin |
Fixed eta constraction issue in compose_witness
|
file |
diff |
annotate
|
| Fri, 14 Dec 2007 17:56:08 +0100 |
wenzelm |
added close_witness;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 23:17:03 +0100 |
wenzelm |
tuned satisfy_thm;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 17:48:34 +0100 |
ballarin |
Removed inst_morphism'; satisfy_thm avoids compose.
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 17:18:32 +0200 |
wenzelm |
proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| 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
|