Tue, 07 Nov 2006 18:14:53 +0100 |
schirmer |
exported intro_locales_tac
|
file |
diff |
annotate
|
Sat, 14 Oct 2006 23:25:54 +0200 |
wenzelm |
export map_elem;
|
file |
diff |
annotate
|
Thu, 12 Oct 2006 22:57:38 +0200 |
wenzelm |
interpretation_in_locale: standalone goal setup;
|
file |
diff |
annotate
|
Wed, 11 Oct 2006 00:31:38 +0200 |
wenzelm |
add_locale(_i): return actual result context;
|
file |
diff |
annotate
|
Tue, 10 Oct 2006 13:59:13 +0200 |
haftmann |
gen_rem(s) abandoned in favour of remove / subtract
|
file |
diff |
annotate
|
Mon, 09 Oct 2006 02:20:04 +0200 |
wenzelm |
removed obsolete note_thmss(_i);
|
file |
diff |
annotate
|
Sat, 07 Oct 2006 01:30:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
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, 09 Aug 2006 00:12:38 +0200 |
wenzelm |
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
|
file |
diff |
annotate
|
Thu, 03 Aug 2006 14:53:57 +0200 |
ballarin |
Updated comments.
|
file |
diff |
annotate
|
Wed, 02 Aug 2006 22:27:01 +0200 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
Thu, 27 Jul 2006 23:28:28 +0200 |
wenzelm |
renamed ProofContext.fix_frees to Variable.fix_frees;
|
file |
diff |
annotate
|
Thu, 27 Jul 2006 13:43:01 +0200 |
wenzelm |
moved basic assumption operations from structure ProofContext to Assumption;
|
file |
diff |
annotate
|
Tue, 25 Jul 2006 21:18:02 +0200 |
wenzelm |
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
|
file |
diff |
annotate
|
Wed, 19 Jul 2006 19:24:02 +0200 |
ballarin |
Strict dfs traversal of imported and registered identifiers.
|
file |
diff |
annotate
|
Tue, 11 Jul 2006 12:24:23 +0200 |
wenzelm |
Name.internal;
|
file |
diff |
annotate
|
Tue, 11 Jul 2006 11:19:28 +0200 |
ballarin |
Witness theorems of interpretations now transfered to current theory.
|
file |
diff |
annotate
|
Sat, 08 Jul 2006 12:54:47 +0200 |
wenzelm |
Element.prove_witness: context;
|
file |
diff |
annotate
|
Fri, 07 Jul 2006 09:39:25 +0200 |
ballarin |
Fixed erroneous check-in.
|
file |
diff |
annotate
|
Fri, 07 Jul 2006 09:28:39 +0200 |
ballarin |
Internal restructuring: identify no longer computes syntax.
|
file |
diff |
annotate
|
Thu, 06 Jul 2006 23:36:40 +0200 |
wenzelm |
removed obsolete locale view;
|
file |
diff |
annotate
|
Tue, 04 Jul 2006 15:45:59 +0200 |
ballarin |
Locales no longer generate views. The following functions have changed
|
file |
diff |
annotate
|
Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
Thu, 22 Jun 2006 07:08:04 +0200 |
ballarin |
Improved handling of defines imported in duplicate.
|
file |
diff |
annotate
|
Tue, 20 Jun 2006 16:46:30 +0200 |
haftmann |
fixed sml/nj value restriction problem
|
file |
diff |
annotate
|
Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
Sat, 17 Jun 2006 19:37:55 +0200 |
wenzelm |
Variable.importT_inst;
|
file |
diff |
annotate
|
Thu, 15 Jun 2006 23:10:45 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
Tue, 13 Jun 2006 23:41:31 +0200 |
wenzelm |
use Drule.unvarify instead of obsolete Drule.freeze_all;
|
file |
diff |
annotate
|