| Thu, 02 Apr 2009 14:49:50 +0200 |
wenzelm |
tuned signature;
|
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
|
| Sat, 07 Mar 2009 12:07:30 +0100 |
wenzelm |
Theory.add_axioms/add_defs: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 16:55:46 +0100 |
wenzelm |
added cancel_proofs, based on task groups of "entered" proofs;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 01:28:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 00:24:07 +0100 |
wenzelm |
simplified join_proofs;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2008 19:27:42 +0100 |
wenzelm |
renamed terminal category "float" to "float_token", to avoid name
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:08:32 +0100 |
wenzelm |
renamed force_proofs to join_proofs;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 00:23:37 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:02:52 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
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
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:06:03 +0100 |
haftmann |
fact table now using name bindings
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 18:25:49 +0100 |
wenzelm |
added force_proofs (based on thms ever passed through enter_thms);
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:31 +0200 |
wenzelm |
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:25 +0200 |
wenzelm |
name_thm etc.: pass position;
|
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
|
| Tue, 05 Aug 2008 13:31:35 +0200 |
wenzelm |
get_fact: report position;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 20:27:38 +0200 |
wenzelm |
removed obsolete note_thms_cmd;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:36 +0200 |
haftmann |
dropped PureThy.note; added PureThy.add_thm
|
file |
diff |
annotate
|