Sun, 09 May 2010 11:43:24 +0100 |
Christian Urban |
fixed the problem with alpha containing splits
|
changeset |
files
|
Sun, 09 May 2010 11:37:19 +0100 |
Christian Urban |
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
|
changeset |
files
|
Fri, 07 May 2010 12:28:11 +0200 |
Cezary Kaliszyk |
Manually added some newer keywords from the distribution
|
changeset |
files
|
Fri, 07 May 2010 12:10:04 +0200 |
Cezary Kaliszyk |
Regularize experiments
|
changeset |
files
|
Thu, 06 May 2010 14:21:10 +0200 |
Cezary Kaliszyk |
alpha_eqvt_tac with prod_rel and prod_fv simps
|
changeset |
files
|
Thu, 06 May 2010 14:14:30 +0200 |
Cezary Kaliszyk |
mem => member
|
changeset |
files
|
Thu, 06 May 2010 14:13:45 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Thu, 06 May 2010 14:13:35 +0200 |
Cezary Kaliszyk |
Fixes for new Isabelle
|
changeset |
files
|
Thu, 06 May 2010 14:13:05 +0200 |
Cezary Kaliszyk |
compound versions with prod_rel and prod_fun, not made default yet.
|
changeset |
files
|
Thu, 06 May 2010 14:10:56 +0200 |
Cezary Kaliszyk |
prod_rel and prod_fv simps
|
changeset |
files
|
Thu, 06 May 2010 14:10:26 +0200 |
Cezary Kaliszyk |
mem => member
|
changeset |
files
|
Thu, 06 May 2010 14:09:56 +0200 |
Cezary Kaliszyk |
prod_rel.simps and Fixed for new isabelle
|
changeset |
files
|
Thu, 06 May 2010 14:09:21 +0200 |
Cezary Kaliszyk |
Fixes for new isabelle
|
changeset |
files
|
Thu, 06 May 2010 13:25:37 +0200 |
Cezary Kaliszyk |
prod_fv and its respectfullness and preservation.
|
changeset |
files
|
Thu, 06 May 2010 10:43:41 +0200 |
Cezary Kaliszyk |
Experiments with equivariance.
|
changeset |
files
|
Wed, 05 May 2010 20:39:56 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Wed, 05 May 2010 20:39:21 +0100 |
Christian Urban |
a bit mor on the pearl journal paper
|
changeset |
files
|
Wed, 05 May 2010 10:24:54 +0100 |
Christian Urban |
solved the problem with equivariance by first eta-normalising the goal
|
changeset |
files
|
Wed, 05 May 2010 09:23:10 +0200 |
Cezary Kaliszyk |
Some cleaning in Term4
|
changeset |
files
|
Tue, 04 May 2010 17:25:58 +0200 |
Cezary Kaliszyk |
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
|
changeset |
files
|
Tue, 04 May 2010 17:15:21 +0200 |
Cezary Kaliszyk |
Move Term4 to NewParser
|
changeset |
files
|
Tue, 04 May 2010 16:59:31 +0200 |
Cezary Kaliszyk |
Fix Term4 for permutation signature change
|
changeset |
files
|
Tue, 04 May 2010 16:44:12 +0200 |
Cezary Kaliszyk |
Move LF to NewParser. Just works.
|
changeset |
files
|
Tue, 04 May 2010 16:42:36 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Tue, 04 May 2010 16:42:28 +0200 |
Cezary Kaliszyk |
ExLetMult
|
changeset |
files
|
Tue, 04 May 2010 16:39:12 +0200 |
Cezary Kaliszyk |
Ex1Rec.
|
changeset |
files
|
Tue, 04 May 2010 16:33:38 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Tue, 04 May 2010 16:33:30 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Tue, 04 May 2010 16:29:11 +0200 |
Cezary Kaliszyk |
ExPS3 in NewParser
|
changeset |
files
|
Tue, 04 May 2010 16:22:21 +0200 |
Cezary Kaliszyk |
Move ExPS8 to new parser.
|
changeset |
files
|