Added and improved macro rules. Also removed the addContractions and addWeakenings objects from lkalgorithms and replaced their uses with macro rules. Moreover, added some set-theoretical convenience methods to FSequents. Some of them could use better names, I think.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2358 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Added an algorithm that can recursively apply a function of type LKProof => LKProof to a proof. Right now it's in the macroRules file, which is perhaps not the most appropriate place. I also added unary equation rules, mainly to see if I could. There are functions to convert between unary and binary equation rules that use the aforementioned recursive algorithm. Lastly, I added a binary Boolean operator =^= to formula occurrences such that o1 =^= o2 iff o1 and o2 are occurrences of the same formula.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2359 85d21ef8-add0-11de-ae77-5bfb9c5a3f34