| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 20:11:49 +0200 |
wenzelm |
Druke.dummy_thm;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 13:47:48 +0200 |
ballarin |
interpretation: unfolding of equations;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:28 +0200 |
wenzelm |
simplified ObjectLogic.atomize;
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:27 +0200 |
wenzelm |
balanced conjunctions;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:56 +0200 |
wenzelm |
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 20:44:11 +0200 |
wenzelm |
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 16:54:57 +0200 |
ballarin |
Interpretation equations applied to attributes;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:32:00 +0200 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
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:19 +0200 |
wenzelm |
avoid clash with Alice keywords;
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 14:53:06 +0200 |
haftmann |
exported interface for intro rules
|
file |
diff |
annotate
|
| Fri, 23 Feb 2007 08:39:24 +0100 |
haftmann |
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
|
file |
diff |
annotate
|
| Mon, 19 Feb 2007 16:44:08 +0100 |
schirmer |
more precise error message in parameter unification
|
file |
diff |
annotate
|
| Sat, 10 Feb 2007 09:26:19 +0100 |
haftmann |
internal interfaces for interpretation and interpret
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:21 +0100 |
wenzelm |
interpretation: attempt to be more serious about name_morphism;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:52 +0100 |
wenzelm |
tuned print_locale output;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:03 +0100 |
wenzelm |
export: added explicit term operation;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:50 +0100 |
wenzelm |
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:25 +0100 |
wenzelm |
Goal.norm/close_result;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:33:09 +0100 |
wenzelm |
*** bad commit -- reverted to previous version ***
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:28:11 +0100 |
wenzelm |
simplified add_thmss;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:15 +0100 |
wenzelm |
simplified add_thmss;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:25 +0100 |
wenzelm |
Element.map_ctxt_attrib;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:19 +0100 |
wenzelm |
tuned morphisms;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:39 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:52:23 +0100 |
wenzelm |
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:38 +0100 |
wenzelm |
notes: proper kind;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 20:50:24 +0100 |
wenzelm |
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:17:01 +0100 |
wenzelm |
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 15:29:55 +0100 |
wenzelm |
simplified Proof.theorem(_i) interface;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 11:58:50 +0100 |
wenzelm |
removed obsolete locale_results;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:40:56 +0100 |
wenzelm |
removed obsolete theorem statements (cf. specification.ML);
|
file |
diff |
annotate
|
| 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
|