2010-05-06 Cezary Kaliszyk compound versions with prod_rel and prod_fun, not made default yet.
2010-05-06 Cezary Kaliszyk prod_rel and prod_fv simps
2010-05-06 Cezary Kaliszyk mem => member
2010-05-06 Cezary Kaliszyk prod_rel.simps and Fixed for new isabelle
2010-05-06 Cezary Kaliszyk Fixes for new isabelle
2010-05-06 Cezary Kaliszyk prod_fv and its respectfullness and preservation.
2010-05-06 Cezary Kaliszyk Experiments with equivariance.
2010-05-05 Christian Urban merged
2010-05-05 Christian Urban a bit mor on the pearl journal paper
2010-05-05 Christian Urban solved the problem with equivariance by first eta-normalising the goal
2010-05-05 Cezary Kaliszyk Some cleaning in Term4
2010-05-04 Cezary Kaliszyk "isabelle make" compiles all examples with newparser/newfv/newalpha only.
2010-05-04 Cezary Kaliszyk Move Term4 to NewParser
2010-05-04 Cezary Kaliszyk Fix Term4 for permutation signature change
2010-05-04 Cezary Kaliszyk Move LF to NewParser. Just works.
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk ExLetMult
2010-05-04 Cezary Kaliszyk Ex1Rec.
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk ExPS3 in NewParser
2010-05-04 Cezary Kaliszyk Move ExPS8 to new parser.
2010-05-04 Cezary Kaliszyk Fix for new isabelle
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk Minor
2010-05-04 Christian Urban increased step counter so that all steps go through
2010-05-04 Christian Urban fixed my error with define_raw_fv
2010-05-04 Christian Urban tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
2010-05-04 Cezary Kaliszyk Separate Term8, as it may work soon.
2010-05-04 Cezary Kaliszyk moved CoreHaskell to NewParser.
2010-05-04 Cezary Kaliszyk ExPS7 in NewParser
2010-05-04 Cezary Kaliszyk Move ExLeroy to New Parser
2010-05-04 Cezary Kaliszyk Move 2 more to NewParser
2010-05-04 Cezary Kaliszyk Move TypeSchemes to NewParser
2010-05-04 Cezary Kaliszyk Move ExLet to NewParser.
2010-05-04 Christian Urban tuned
2010-05-04 Christian Urban roll back of the last commit (there was a difference)
2010-05-04 Christian Urban tuned
2010-05-04 Christian Urban to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
2010-05-04 Christian Urban merged
2010-05-04 Christian Urban some preliminary changes to the pearl-jv paper
2010-05-03 Christian Urban some preliminary notes of the abstract (qpaper); still need to see the motivating example
2010-05-03 Cezary Kaliszyk Added cheats to classical
2010-05-03 Cezary Kaliszyk Ex2 moved to new parser.
2010-05-03 Cezary Kaliszyk alpha_eqvt_tac fixed to work when the existential is not at the top level.
2010-05-03 Cezary Kaliszyk SingleLet and Ex3 work with NewParser.
2010-05-03 Cezary Kaliszyk Comment
2010-05-03 Cezary Kaliszyk Another example where only alpha_eqvt fails.
2010-05-03 Cezary Kaliszyk Register only non-looping rules in eq_iff
2010-05-03 Cezary Kaliszyk Equivariance fails for single let?
2010-05-03 Cezary Kaliszyk NewParser
2010-05-03 Cezary Kaliszyk Introduce eq_iff_simp to match the one from Parser.
2010-05-03 Cezary Kaliszyk remove tracing
2010-05-03 Cezary Kaliszyk Cheat support equations in new parser
2010-05-03 Cezary Kaliszyk Remove dependency on NewFv
2010-05-03 Cezary Kaliszyk Fix Parser
2010-05-03 Cezary Kaliszyk Add explicit cheats in NewParser and comment out the examples for outside use.
2010-05-03 Cezary Kaliszyk Fix Datatype_Aux calls in NewParser.
2010-05-03 Cezary Kaliszyk Move old fv_alpha_export to Fv.
2010-05-02 Christian Urban moved old parser and old fv back into their original places; isabelle make works again
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip