Nominal/Ex/SingleLet.thy
Mon, 21 Jun 2010 06:47:40 +0100 Christian Urban merged with main line
Fri, 11 Jun 2010 03:02:42 +0200 Christian Urban also symmetry
Wed, 09 Jun 2010 15:14:16 +0200 Christian Urban transitivity proofs done
Mon, 07 Jun 2010 11:46:26 +0200 Christian Urban merged
Mon, 07 Jun 2010 11:43:01 +0200 Christian Urban work on transitivity proof
Wed, 02 Jun 2010 11:37:51 +0200 Christian Urban fixed problem with bn_info
Tue, 01 Jun 2010 15:21:01 +0200 Christian Urban equivariance done
Tue, 01 Jun 2010 15:01:05 +0200 Christian Urban smaller code for raw-eqvt proofs
Mon, 31 May 2010 19:57:29 +0200 Christian Urban all raw definitions are defined using function
Thu, 27 May 2010 18:40:10 +0200 Christian Urban merged
Thu, 27 May 2010 18:37:52 +0200 Christian Urban intermediate state
Tue, 25 May 2010 00:24:41 +0100 Christian Urban added slides
Mon, 24 May 2010 20:02:37 +0100 Christian Urban alpha works now
Sun, 23 May 2010 02:15:24 +0100 Christian Urban started to work on alpha
Sat, 22 May 2010 13:51:47 +0100 Christian Urban properly exported bn_descr
Fri, 21 May 2010 11:40:18 +0100 Christian Urban hving a working fv-definition without the export
Fri, 21 May 2010 05:58:23 +0100 Christian Urban tuned
Thu, 20 May 2010 21:23:53 +0100 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Sun, 20 Jun 2010 02:37:58 +0100 Christian Urban fixed example
Mon, 07 Jun 2010 11:33:00 +0200 Christian Urban improved abstract, some tuning
Thu, 27 May 2010 18:30:26 +0200 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Mon, 17 May 2010 16:25:45 +0100 Christian Urban minor tuning
Wed, 12 May 2010 16:59:53 +0100 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
Wed, 12 May 2010 16:33:25 +0100 Christian Urban moved the data-transformation into the parser
Wed, 12 May 2010 14:47:52 +0100 Christian Urban ingnored parameters in equivariance; added a proper interface to be called from ML
Wed, 12 May 2010 13:43:48 +0100 Christian Urban properly exported defined bn-functions
Tue, 11 May 2010 18:20:25 +0200 Cezary Kaliszyk Include raw permutation definitions in eqvt
Tue, 11 May 2010 17:16:57 +0200 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Wed, 05 May 2010 10:24:54 +0100 Christian Urban solved the problem with equivariance by first eta-normalising the goal
Mon, 03 May 2010 15:36:47 +0200 Cezary Kaliszyk SingleLet and Ex3 work with NewParser.
Mon, 03 May 2010 14:03:30 +0200 Cezary Kaliszyk Equivariance fails for single let?
Tue, 20 Apr 2010 18:24:50 +0200 Christian Urban renamed Ex1.thy to SingleLet.thy
less more (0) tip