2010-03-11 Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 16:15:29 +0100] rev 1425
Fixes for term1 for new alpha. Still not able to show support equations.
2010-03-11 merged
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 16:12:15 +0100] rev 1424
merged
2010-03-11 finally the proof that new and old alpha agree
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 15:10:07 +0100] rev 1423
finally the proof that new and old alpha agree
2010-03-11 Remove "_raw" from lifted theorems.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 15:11:57 +0100] rev 1422
Remove "_raw" from lifted theorems.
2010-03-11 looking at trm5_equivp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 14:09:54 +0100] rev 1421
looking at trm5_equivp
2010-03-11 The cheats described explicitely.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 14:05:36 +0100] rev 1420
The cheats described explicitely.
2010-03-11 The alpha5_eqvt tactic works if I manage to build the goal.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 13:44:54 +0100] rev 1419
The alpha5_eqvt tactic works if I manage to build the goal.
2010-03-11 With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 13:34:45 +0100] rev 1418
With the 4 cheats, all examples fully lift.
2010-03-11 Lift alpha_bn_constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 12:30:53 +0100] rev 1417
Lift alpha_bn_constants.
2010-03-11 Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 12:26:24 +0100] rev 1416
Lifting constants.
2010-03-11 Proper error message.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:41:27 +0100] rev 1415
Proper error message.
2010-03-11 Lifting constants works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:32:37 +0100] rev 1414
Lifting constants works for all examples.
2010-03-11 Remove tracing from fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:56 +0100] rev 1413
Remove tracing from fv/alpha.
2010-03-11 Equivp working only on the standard alpha-equivalences.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:18 +0100] rev 1412
Equivp working only on the standard alpha-equivalences.
2010-03-11 explicit cheat_fv_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:20:50 +0100] rev 1411
explicit cheat_fv_eqvt
2010-03-11 extract build_eqvts_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:15:14 +0100] rev 1410
extract build_eqvts_tac.
2010-03-11 build_eqvts no longer requires permutations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:39:29 +0100] rev 1409
build_eqvts no longer requires permutations.
2010-03-11 Add explicit alpha_eqvt_cheat.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:22:24 +0100] rev 1408
Add explicit alpha_eqvt_cheat.
2010-03-11 Export tactic out of alpha_eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:10:23 +0100] rev 1407
Export tactic out of alpha_eqvt.
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:59:08 +0100] rev 1406
merge
2010-03-10 More tries about the proofs in trm5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:58:14 +0100] rev 1405
More tries about the proofs in trm5
2010-03-10 merged
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:51:15 +0100] rev 1404
merged
2010-03-10 almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:50:42 +0100] rev 1403
almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10 alpha_equivp for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:40:15 +0100] rev 1402
alpha_equivp for trm5
2010-03-10 Undoing mistakenly committed parser experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:34:13 +0100] rev 1401
Undoing mistakenly committed parser experiments.
2010-03-10 alpha_eqvt for recursive term1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:32:51 +0100] rev 1400
alpha_eqvt for recursive term1.
2010-03-10 Looking at alpha_eqvt for term5, not much progress.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 14:47:04 +0100] rev 1399
Looking at alpha_eqvt for term5, not much progress.
2010-03-10 Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 14:24:27 +0100] rev 1398
Reordered examples in Test.
2010-03-10 Allows multiple bindings with same lhs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 13:29:12 +0100] rev 1397
Allows multiple bindings with same lhs.
2010-03-10 Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 13:10:00 +0100] rev 1396
Linked parser to fv and alpha.
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 12:53:44 +0100] rev 1395
merge
2010-03-10 A minor fix for shallow binders. LF works again.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 12:53:30 +0100] rev 1394
A minor fix for shallow binders. LF works again.
2010-03-10 merged
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 12:48:55 +0100] rev 1393
merged
2010-03-10 parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 12:48:38 +0100] rev 1392
parser produces ordered bn-fun information
2010-03-10 Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 11:39:28 +0100] rev 1391
Testing equalities in trm5, all seems good.
2010-03-10 Fv&Alpha seem to work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 11:19:59 +0100] rev 1390
Fv&Alpha seem to work.
2010-03-10 include alpha in the definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 10:47:21 +0100] rev 1389
include alpha in the definitions.
2010-03-10 Filled the algorithm for alpha_bn_arg
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 10:11:20 +0100] rev 1388
Filled the algorithm for alpha_bn_arg
2010-03-10 rhs of alpha_bn, and template for the arguments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:58:43 +0100] rev 1387
rhs of alpha_bn, and template for the arguments.
2010-03-10 alpha_bn_constr template
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:45:38 +0100] rev 1386
alpha_bn_constr template
2010-03-10 exported template for alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:36:07 +0100] rev 1385
exported template for alpha_bn
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:10:11 +0100] rev 1384
merge
2010-03-10 Use alpha_bns in normal alpha defs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:09:52 +0100] rev 1383
Use alpha_bns in normal alpha defs.
2010-03-10 alpha_bn_frees
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 08:44:19 +0100] rev 1382
alpha_bn_frees
2010-03-09 merged
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 22:10:10 +0100] rev 1381
merged
2010-03-09 added bn-information, but it is not yet ordered according to the dts
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 22:08:38 +0100] rev 1380
added bn-information, but it is not yet ordered according to the dts
2010-03-09 Separate lists for separate constructors, to match bn_eqs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 21:22:22 +0100] rev 1379
Separate lists for separate constructors, to match bn_eqs.
2010-03-09 All examples should work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 17:25:35 +0100] rev 1378
All examples should work.
2010-03-09 Fix to get old alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 17:02:29 +0100] rev 1377
Fix to get old alpha.
2010-03-09 Separate primrecs in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 16:57:51 +0100] rev 1376
Separate primrecs in Fv.
2010-03-09 A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 16:24:39 +0100] rev 1375
A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-09 Trying to prove that old alpha is the same as new recursive one. Lets still to do.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 11:36:40 +0100] rev 1374
Trying to prove that old alpha is the same as new recursive one. Lets still to do.
2010-03-09 fv_bi and alpha_bi
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 11:06:57 +0100] rev 1373
fv_bi and alpha_bi
2010-03-09 merged
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 09:55:19 +0100] rev 1372
merged
2010-03-09 added first test about new compat
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 09:54:58 +0100] rev 1371
added first test about new compat
2010-03-09 fv_compat
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 09:38:49 +0100] rev 1370
fv_compat
2010-03-09 added another compat example
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 08:46:55 +0100] rev 1369
added another compat example
2010-03-08 added a test-file for compatibility
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 20:18:27 +0100] rev 1368
added a test-file for compatibility
2010-03-08 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 16:11:42 +0100] rev 1367
added compat definitions to some examples
2010-03-08 Proper recognition of atoms and atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 15:28:25 +0100] rev 1366
Proper recognition of atoms and atom sets.
2010-03-08 deleted comments about "weird"
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:06:14 +0100] rev 1365
deleted comments about "weird"
2010-03-08 merged
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:01:26 +0100] rev 1364
merged
2010-03-08 updated to new Isabelle
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:01:01 +0100] rev 1363
updated to new Isabelle
2010-03-08 Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 14:31:04 +0100] rev 1362
Term5 written as nominal_datatype is the recursive let.
2010-03-08 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:25:57 +0100] rev 1361
With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-08 More fine-grained nominal restriction for debugging.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:12:15 +0100] rev 1360
More fine-grained nominal restriction for debugging.
2010-03-08 Fix permutation addition.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:10:43 +0100] rev 1359
Fix permutation addition.
2010-03-08 Update the comments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:33:55 +0100] rev 1358
Update the comments
2010-03-08 Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:08:31 +0100] rev 1357
Gather bindings with same binder, and generate only one permutation for them.
2010-03-08 Undo effects of simp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 02:40:16 +0100] rev 1356
Undo effects of simp.
2010-03-07 merged
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:57 +0100] rev 1355
merged
2010-03-07 updated to renamings in Isabelle
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:12 +0100] rev 1354
updated to renamings in Isabelle
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:56:58 +0100] rev 1353
merged
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:34 +0100] rev 1352
merged
2010-03-04 more proofs in Abs and work on Core Haskell
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:21 +0100] rev 1351
more proofs in Abs and work on Core Haskell
2010-03-03 added a lemma that permutations can be represented as sums of swapping
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 19:10:40 +0100] rev 1350
added a lemma that permutations can be represented as sums of swapping
2010-03-05 Still unable to show supp=fv for let with one existential.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 18:14:04 +0100] rev 1349
Still unable to show supp=fv for let with one existential.
2010-03-05 Ported LF to the parser interface.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 17:09:48 +0100] rev 1348
Ported LF to the parser interface.
2010-03-05 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:56:19 +0100] rev 1347
merge
2010-03-05 Lift fv and bn eqvts; no need to lift alpha_eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:55:21 +0100] rev 1346
Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Not much progress about the single existential let case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 13:04:47 +0100] rev 1345
Not much progress about the single existential let case.
2010-03-05 Fixed LF for one quantifier over 2 premises.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 10:23:40 +0100] rev 1344
Fixed LF for one quantifier over 2 premises.
2010-03-05 Trying to fix the proofs for the single existential... So far failed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 09:41:22 +0100] rev 1343
Trying to fix the proofs for the single existential... So far failed.
2010-03-04 Lift distinct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 18:57:23 +0100] rev 1342
Lift distinct.
2010-03-04 Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:55:53 +0100] rev 1341
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:15:44 +0100] rev 1340
Lift BV,FV,Permutations and injection :).
2010-03-04 Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 12:00:11 +0100] rev 1339
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04 A version that just leaves the supp/\supp goal. Obviously not true.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 11:16:36 +0100] rev 1338
A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Prove symp and transp of weird without the supp /\ supp = {} assumption.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 10:59:52 +0100] rev 1337
Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:51:47 +0100] rev 1336
merge
2010-03-03 Experiments with proving weird transp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:49:34 +0100] rev 1335
Experiments with proving weird transp
2010-03-03 Code for solving symp goals with multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:47:29 +0100] rev 1334
Code for solving symp goals with multiple existentials.
2010-03-03 reflp for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 15:28:25 +0100] rev 1333
reflp for multiple quantifiers.
2010-03-03 fixed mess in Test.thy
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 14:46:14 +0100] rev 1332
fixed mess in Test.thy
2010-03-03 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 14:22:58 +0100] rev 1331
Fix eqvt for multiple quantifiers.
2010-03-03 only tuned
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:48:05 +0100] rev 1330
only tuned
2010-03-03 merged
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:47:06 +0100] rev 1329
merged
2010-03-03 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:45:55 +0100] rev 1328
start of paper - does not compile yet
2010-03-03 added ACM style file for ICFP
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 11:50:25 +0100] rev 1327
added ACM style file for ICFP
2010-03-03 weird eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 11:42:15 +0100] rev 1326
weird eqvt
2010-03-03 Add the supp intersection conditions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 10:39:43 +0100] rev 1325
Add the supp intersection conditions.
2010-03-02 Comment out the part that does not work with 2 quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 21:43:27 +0100] rev 1324
Comment out the part that does not work with 2 quantifiers.
2010-03-02 Fixes for the fv problem and alpha problem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 21:10:04 +0100] rev 1323
Fixes for the fv problem and alpha problem.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 20:14:21 +0100] rev 1322
merged
2010-03-02 preliinary test about alpha-weirdo
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 20:11:56 +0100] rev 1321
preliinary test about alpha-weirdo
2010-03-02 Another problem with permutations in alpha and possibly also in fv
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 18:57:26 +0100] rev 1320
Another problem with permutations in alpha and possibly also in fv
2010-03-02 potential problem with the phd-example, where two permutations are generated, but only one is used
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 18:48:20 +0100] rev 1319
potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 19:48:44 +0100] rev 1318
Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:48:56 +0100] rev 1317
merge
2010-03-02 Porting from Lift to Parser; until defining the Quotient type.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:48:41 +0100] rev 1316
Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:11:58 +0100] rev 1315
Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Include the raw eqvt lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:11:19 +0100] rev 1314
Include the raw eqvt lemmas.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 16:04:48 +0100] rev 1313
merged
2010-03-02 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 16:03:19 +0100] rev 1312
added some more examples from Peter Sewell's bestiary
2010-03-02 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:13:00 +0100] rev 1311
merge
2010-03-02 Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:12:50 +0100] rev 1310
Minor
2010-03-02 Working bv_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:11:41 +0100] rev 1309
Working bv_eqvt
2010-03-02 Moving wrappers out of Lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:10:47 +0100] rev 1308
Moving wrappers out of Lift.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 15:07:27 +0100] rev 1307
merged
2010-03-02 added distinctness of perms
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 15:05:50 +0100] rev 1306
added distinctness of perms
(0) -1000 -120 +120 +1000 tip