2010-05-03 |
Cezary Kaliszyk |
Move old fv_alpha_export to Fv.
|
file |
diff |
annotate
|
2010-05-02 |
Christian Urban |
moved old parser and old fv back into their original places; isabelle make works again
|
file |
diff |
annotate
| base
|
2010-04-20 |
Christian Urban |
renamed Ex1.thy to SingleLet.thy
|
file |
diff |
annotate
|
2010-04-19 |
Christian Urban |
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
|
file |
diff |
annotate
|
2010-04-14 |
Cezary Kaliszyk |
Separate alpha_definition.
|
file |
diff |
annotate
|
2010-04-14 |
Cezary Kaliszyk |
Separate define_fv.
|
file |
diff |
annotate
|
2010-04-14 |
Cezary Kaliszyk |
Initial cleaning/reorganization in Fv.
|
file |
diff |
annotate
|
2010-04-11 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-04-04 |
Christian Urban |
separated general nominal theory into separate folder
|
file |
diff |
annotate
|
2010-04-01 |
Cezary Kaliszyk |
Let with multiple bindings.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Lets finally abstract lists.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Equivariance when bn functions are lists.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Accepts lists in FV.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Automatically compute support if only one type of Abs is present in the type.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Manually proved TySch support; All properties of TySch now true.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Generalize Abs_eq_iff.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Initial proof modifications for alpha_res
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Fv/Alpha now takes into account Alpha_Type given from the parser.
|
file |
diff |
annotate
|
2010-03-27 |
Cezary Kaliszyk |
Minor cleaning.
|
file |
diff |
annotate
|
2010-03-26 |
Cezary Kaliszyk |
Fixed renamings.
|
file |
diff |
annotate
|
2010-03-26 |
Cezary Kaliszyk |
Removed remaining cheats + some cleaning.
|
file |
diff |
annotate
|
2010-03-26 |
Cezary Kaliszyk |
Removed another cheat and cleaned the code a bit.
|
file |
diff |
annotate
|
2010-03-25 |
Cezary Kaliszyk |
Proper bn_rsp, for bn functions calling each other.
|
file |
diff |
annotate
|
2010-03-25 |
Cezary Kaliszyk |
Gathering things to prove by induction together; removed cheat_bn_eqvt.
|
file |
diff |
annotate
|
2010-03-24 |
Cezary Kaliszyk |
Support proof modification for Core Haskell.
|
file |
diff |
annotate
|
2010-03-24 |
Cezary Kaliszyk |
Compute Fv for non-recursive bn functions calling other bn functions
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Modification to Core Haskell to make it accepted with an empty binding function.
|
file |
diff |
annotate
|
2010-03-22 |
Cezary Kaliszyk |
equivp_cheat can be removed for all one-permutation examples.
|
file |
diff |
annotate
|