Thu, 06 May 2010 14:10:26 +0200 Cezary Kaliszyk mem => member
Thu, 06 May 2010 14:09:56 +0200 Cezary Kaliszyk prod_rel.simps and Fixed for new isabelle
Thu, 06 May 2010 14:09:21 +0200 Cezary Kaliszyk Fixes for new isabelle
Thu, 06 May 2010 13:25:37 +0200 Cezary Kaliszyk prod_fv and its respectfullness and preservation.
Thu, 06 May 2010 10:43:41 +0200 Cezary Kaliszyk Experiments with equivariance.
Wed, 05 May 2010 20:39:56 +0100 Christian Urban merged
Wed, 05 May 2010 20:39:21 +0100 Christian Urban a bit mor on the pearl journal paper
Wed, 05 May 2010 10:24:54 +0100 Christian Urban solved the problem with equivariance by first eta-normalising the goal
Wed, 05 May 2010 09:23:10 +0200 Cezary Kaliszyk Some cleaning in Term4
Tue, 04 May 2010 17:25:58 +0200 Cezary Kaliszyk "isabelle make" compiles all examples with newparser/newfv/newalpha only.
Tue, 04 May 2010 17:15:21 +0200 Cezary Kaliszyk Move Term4 to NewParser
Tue, 04 May 2010 16:59:31 +0200 Cezary Kaliszyk Fix Term4 for permutation signature change
Tue, 04 May 2010 16:44:12 +0200 Cezary Kaliszyk Move LF to NewParser. Just works.
Tue, 04 May 2010 16:42:36 +0200 Cezary Kaliszyk merge
Tue, 04 May 2010 16:42:28 +0200 Cezary Kaliszyk ExLetMult
Tue, 04 May 2010 16:39:12 +0200 Cezary Kaliszyk Ex1Rec.
Tue, 04 May 2010 16:33:38 +0200 Cezary Kaliszyk merge
Tue, 04 May 2010 16:33:30 +0200 Cezary Kaliszyk merge
Tue, 04 May 2010 16:29:11 +0200 Cezary Kaliszyk ExPS3 in NewParser
Tue, 04 May 2010 16:22:21 +0200 Cezary Kaliszyk Move ExPS8 to new parser.
Tue, 04 May 2010 16:30:31 +0200 Cezary Kaliszyk Fix for new isabelle
Tue, 04 May 2010 16:18:07 +0200 Cezary Kaliszyk merge
Tue, 04 May 2010 16:17:46 +0200 Cezary Kaliszyk Minor
Tue, 04 May 2010 14:38:07 +0100 Christian Urban increased step counter so that all steps go through
Tue, 04 May 2010 14:33:50 +0100 Christian Urban fixed my error with define_raw_fv
Tue, 04 May 2010 14:25:22 +0100 Christian Urban tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Tue, 04 May 2010 14:21:18 +0200 Cezary Kaliszyk Separate Term8, as it may work soon.
Tue, 04 May 2010 14:13:18 +0200 Cezary Kaliszyk moved CoreHaskell to NewParser.
Tue, 04 May 2010 13:52:40 +0200 Cezary Kaliszyk ExPS7 in NewParser
Tue, 04 May 2010 12:34:33 +0200 Cezary Kaliszyk Move ExLeroy to New Parser
Tue, 04 May 2010 11:22:22 +0200 Cezary Kaliszyk Move 2 more to NewParser
Tue, 04 May 2010 11:12:09 +0200 Cezary Kaliszyk Move TypeSchemes to NewParser
Tue, 04 May 2010 11:08:30 +0200 Cezary Kaliszyk Move ExLet to NewParser.
Tue, 04 May 2010 07:22:33 +0100 Christian Urban tuned
Tue, 04 May 2010 06:24:54 +0100 Christian Urban roll back of the last commit (there was a difference)
Tue, 04 May 2010 06:05:13 +0100 Christian Urban tuned
Tue, 04 May 2010 06:02:45 +0100 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
Tue, 04 May 2010 05:36:55 +0100 Christian Urban merged
Tue, 04 May 2010 05:36:43 +0100 Christian Urban some preliminary changes to the pearl-jv paper
Mon, 03 May 2010 08:52:15 +0100 Christian Urban some preliminary notes of the abstract (qpaper); still need to see the motivating example
Mon, 03 May 2010 15:47:30 +0200 Cezary Kaliszyk Added cheats to classical
Mon, 03 May 2010 15:38:20 +0200 Cezary Kaliszyk Ex2 moved to new parser.
Mon, 03 May 2010 15:37:21 +0200 Cezary Kaliszyk alpha_eqvt_tac fixed to work when the existential is not at the top level.
Mon, 03 May 2010 15:36:47 +0200 Cezary Kaliszyk SingleLet and Ex3 work with NewParser.
Mon, 03 May 2010 15:13:15 +0200 Cezary Kaliszyk Comment
Mon, 03 May 2010 14:31:11 +0200 Cezary Kaliszyk Another example where only alpha_eqvt fails.
Mon, 03 May 2010 14:30:37 +0200 Cezary Kaliszyk Register only non-looping rules in eq_iff
Mon, 03 May 2010 14:03:30 +0200 Cezary Kaliszyk Equivariance fails for single let?
Mon, 03 May 2010 13:42:44 +0200 Cezary Kaliszyk NewParser
Mon, 03 May 2010 12:24:27 +0200 Cezary Kaliszyk Introduce eq_iff_simp to match the one from Parser.
Mon, 03 May 2010 11:43:27 +0200 Cezary Kaliszyk remove tracing
Mon, 03 May 2010 11:43:08 +0200 Cezary Kaliszyk Cheat support equations in new parser
Mon, 03 May 2010 11:37:44 +0200 Cezary Kaliszyk Remove dependency on NewFv
Mon, 03 May 2010 11:35:38 +0200 Cezary Kaliszyk Fix Parser
Mon, 03 May 2010 10:15:23 +0200 Cezary Kaliszyk Add explicit cheats in NewParser and comment out the examples for outside use.
Mon, 03 May 2010 09:57:05 +0200 Cezary Kaliszyk Fix Datatype_Aux calls in NewParser.
Mon, 03 May 2010 09:55:43 +0200 Cezary Kaliszyk Move old fv_alpha_export to Fv.
Mon, 03 May 2010 00:01:12 +0100 Christian Urban moved old parser and old fv back into their original places; isabelle make works again
Mon, 03 May 2010 00:00:33 +0100 Christian Urban slight tuning
Sun, 02 May 2010 21:15:52 +0100 Christian Urban simplified the supp-of-finite-sets proof
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip