| Sun, 26 Apr 2009 00:42:49 +0200 |
Christian Urban |
deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:07:10 +0100 |
berghofe |
Replaced Logic.unvarify by Variable.import_terms to make declaration of
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 18:27:43 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:01 +0200 |
wenzelm |
proper dynamic facts for eqvts, freshs, bijs;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2008 21:59:48 +0100 |
wenzelm |
update_context: always store as "Nominal.eqvts";
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:44 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:28:08 +0100 |
wenzelm |
auxiliary dynamic_thm(s) for fact lookup;
|
file |
diff |
annotate
|
| Thu, 13 Sep 2007 23:58:38 +0200 |
urbanc |
some cleaning up to do with contexts
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:22:51 +0200 |
wenzelm |
avoid low-level tsig;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 15:09:33 +0200 |
narboux |
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|