Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
Fri, 02 Oct 2009 21:39:06 +0200 |
wenzelm |
clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 17:21:11 +0100 |
wenzelm |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
file |
diff |
annotate
|
Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 21:37:18 +0100 |
wenzelm |
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 15:54:19 +0100 |
wenzelm |
Assumption.local_prems_of;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 14:30:23 +0100 |
wenzelm |
axiomatization: more precise treatment of binding;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 15:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
Fri, 19 Dec 2008 16:39:23 +0100 |
ballarin |
All logics ported to new locales.
|
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
|
Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
file |
diff |
annotate
|
Mon, 24 Nov 2008 18:04:21 +0100 |
ballarin |
Enable switching to new locales during session.
|
file |
diff |
annotate
|
Mon, 24 Nov 2008 14:23:04 +0100 |
ballarin |
More ramifications of removal of 'includes' element.
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 00:03:55 +0100 |
wenzelm |
removed traces of former 'includes' element;
|
file |
diff |
annotate
|
Mon, 17 Nov 2008 17:00:22 +0100 |
haftmann |
adjusted locale signature to *_cmd convention
|
file |
diff |
annotate
|
Fri, 14 Nov 2008 08:50:09 +0100 |
haftmann |
Name.is_nothing
|
file |
diff |
annotate
|
Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
file |
diff |
annotate
|
Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 17:47:38 +0200 |
wenzelm |
axiomatization is now global-only;
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 22:20:20 +0200 |
wenzelm |
ProofDisplay.print_results;
|
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:30 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
Wed, 13 Aug 2008 20:57:33 +0200 |
wenzelm |
ProofDisplay.theory_results;
|
file |
diff |
annotate
|
Wed, 09 Apr 2008 21:49:37 +0200 |
wenzelm |
print_consts only for external specifications;
|
file |
diff |
annotate
|
Thu, 20 Mar 2008 00:20:49 +0100 |
wenzelm |
renamed former get_thms(_silent) to get_fact(_silent);
|
file |
diff |
annotate
|
Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
Sat, 10 Nov 2007 14:31:21 +0100 |
wenzelm |
notation: improved ProofContext.read_const does the job;
|
file |
diff |
annotate
|
Fri, 26 Oct 2007 22:10:43 +0200 |
wenzelm |
notation: associate syntax to checked-unchecked term;
|
file |
diff |
annotate
|
Sat, 13 Oct 2007 17:16:39 +0200 |
wenzelm |
renamed LocalTheory.def to LocalTheory.define;
|
file |
diff |
annotate
|
Fri, 12 Oct 2007 20:21:57 +0200 |
wenzelm |
more informative TheoryTarget.peek operation;
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 21:10:42 +0200 |
wenzelm |
removed unused/impure quiet_mode;
|
file |
diff |
annotate
|
Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
Tue, 09 Oct 2007 17:10:36 +0200 |
wenzelm |
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file |
diff |
annotate
|
Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
Wed, 26 Sep 2007 22:21:02 +0200 |
wenzelm |
read/check_specification: free_dummy_patterns;
|
file |
diff |
annotate
|
Wed, 26 Sep 2007 19:17:59 +0200 |
wenzelm |
read/check_specification: proper type inference across multiple sections, result is in closed form;
|
file |
diff |
annotate
|
Sat, 22 Sep 2007 17:45:58 +0200 |
wenzelm |
ProofContext.mode_abbrev;
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
Fri, 07 Sep 2007 22:13:49 +0200 |
wenzelm |
theorem: apply hook last;
|
file |
diff |
annotate
|
Thu, 06 Sep 2007 12:30:11 +0200 |
wenzelm |
theorem hooks: apply in declaration order;
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 19:45:45 +0200 |
wenzelm |
TheoremHook: fixed copy-paste mistake;
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 18:03:16 +0200 |
berghofe |
- theorem(_i) now also takes "interactive" flag as argument
|
file |
diff |
annotate
|
Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
Thu, 10 May 2007 15:50:28 +0200 |
berghofe |
Changed name of raw definition.
|
file |
diff |
annotate
|
Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
file |
diff |
annotate
|
Tue, 12 Dec 2006 20:49:19 +0100 |
wenzelm |
LocalTheory.abbrev;
|
file |
diff |
annotate
|