| 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
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2007 07:32:23 +0200 |
urbanc |
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
|
file |
diff |
annotate
|
| Mon, 02 Apr 2007 23:24:52 +0200 |
narboux |
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 18:25:23 +0200 |
urbanc |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 11:17:32 +0100 |
urbanc |
clarified an error-message
|
file |
diff |
annotate
|
| Mon, 12 Mar 2007 16:25:39 +0100 |
narboux |
removes some unused code that used to try to derive a simpler version of the eqvt lemmas
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 15:28:22 +0100 |
urbanc |
major update of the nominal package; there is now an infrastructure
|
file |
diff |
annotate
|
| Thu, 08 Feb 2007 17:22:22 +0100 |
urbanc |
added get-functions
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 15:12:18 +0100 |
urbanc |
fixed two stupid bugs of SML to do with the value restriction and missing type
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
file |
diff |
annotate
|