| Wed, 25 Apr 2007 21:29:14 +0200 |
narboux |
add the lemma supp_eqvt and put the right attribute
|
changeset |
files
|
| Wed, 25 Apr 2007 17:50:48 +0200 |
nipkow |
new lemma splice_length
|
changeset |
files
|
| Wed, 25 Apr 2007 15:38:56 +0200 |
narboux |
fix sml compilation
|
changeset |
files
|
| Wed, 25 Apr 2007 15:26:01 +0200 |
berghofe |
Moved function params_of to inductive_package.ML.
|
changeset |
files
|
| Wed, 25 Apr 2007 15:25:22 +0200 |
berghofe |
Moved functions infer_intro_vars, arities_of, params_of, and
|
changeset |
files
|
| Wed, 25 Apr 2007 15:24:15 +0200 |
berghofe |
Added functions arities_of, params_of, partition_rules, and
|
changeset |
files
|
| Wed, 25 Apr 2007 15:22:57 +0200 |
berghofe |
eqvt_tac now instantiates introduction rules before applying them.
|
changeset |
files
|
| Tue, 24 Apr 2007 18:06:04 +0200 |
narboux |
update fresh_fun_simp for debugging purposes
|
changeset |
files
|
| Tue, 24 Apr 2007 17:16:55 +0200 |
narboux |
fixes last commit
|
changeset |
files
|
| Tue, 24 Apr 2007 16:44:11 +0200 |
narboux |
add two lemmas dealing with freshness on permutations.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:19:33 +0200 |
berghofe |
Added datatype_case.ML and nominal_fresh_fun.ML.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:18:42 +0200 |
berghofe |
Added datatype_case.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:18:09 +0200 |
berghofe |
Added intro / elim rules for prod_case.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:17:22 +0200 |
berghofe |
sum_case is now authentic.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:15:52 +0200 |
berghofe |
Adapted to new parse translation for case expressions.
|
changeset |
files
|