2010-05-12 Christian Urban properly exported defined bn-functions
2010-05-11 Cezary Kaliszyk Include raw permutation definitions in eqvt
2010-05-11 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
2010-05-11 Christian Urban a bit for the introduction of the q-paper
2010-05-11 Christian Urban added some of the quotient literature; a bit more to the qpaper
2010-05-10 Christian Urban fixed a problem with non-existant alphas2
2010-05-10 Christian Urban added comment about bind_set
2010-05-10 Christian Urban fixing bind_set problem
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Term8 comment
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Restore set bindings in CoreHaskell
2010-05-10 Cezary Kaliszyk Recursive examples with relation composition
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk prod_rel and prod_fv eqvt and mono
2010-05-10 Cezary Kaliszyk ExLetRec
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Parser changes for compound relations
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Use mk_compound_fv' and mk_compound_rel'
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Membership in a pair of lists.
2010-05-10 Cezary Kaliszyk Synchronize FSet with repository
2010-05-09 Christian Urban tuned file names for examples
2010-05-09 Christian Urban cleaned up a bit the examples; added equivariance to all examples
2010-05-09 Christian Urban fixed the problem with alpha containing splits
2010-05-09 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
2010-05-07 Cezary Kaliszyk Manually added some newer keywords from the distribution
2010-05-07 Cezary Kaliszyk Regularize experiments
2010-05-06 Cezary Kaliszyk alpha_eqvt_tac with prod_rel and prod_fv simps
2010-05-06 Cezary Kaliszyk mem => member
2010-05-06 Cezary Kaliszyk merge
2010-05-06 Cezary Kaliszyk Fixes for new Isabelle
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
2010-05-02 Christian Urban slight tuning
2010-05-02 Christian Urban simplified the supp-of-finite-sets proof
2010-05-02 Christian Urban tried to add some comments in the huge(!) nominal2_cmd function
2010-05-02 Christian Urban replaced make_pair with library function HOLogic.mk_prod
2010-05-02 Christian Urban removed duplicate eqvt attribute
2010-05-02 Christian Urban attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-05-01 Christian Urban merged
2010-05-01 Christian Urban tuned
2010-04-30 Christian Urban replaced hide by the new hide_const
2010-04-30 Christian Urban generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
2010-04-30 Christian Urban added lemmas establishing the support of finite sets of finitely supported elements
2010-04-30 Christian Urban added eqvt-lemmas for Bex, Ball and Union
2010-04-30 Cezary Kaliszyk NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Cezary Kaliszyk Merged nominal_datatype into NewParser until eqvts
2010-04-30 Cezary Kaliszyk more parser/new parser synchronization.
2010-04-30 Cezary Kaliszyk Simplify old parser for integration
2010-04-30 Cezary Kaliszyk merge
2010-04-30 Cezary Kaliszyk Change signature of fv and alpha generation.
2010-04-30 Christian Urban reorganised eqvt-file (now uses perm_simp already)
(0) -1000 -112 +112 +1000 tip