Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal-General/Nominal2_Eqvt.thy
Sun, 02 May 2010 16:00:52 +0100 Christian Urban removed duplicate eqvt attribute file | diff | annotate
Fri, 30 Apr 2010 14:21:18 +0100 Christian Urban added eqvt-lemmas for Bex, Ball and Union file | diff | annotate
Fri, 30 Apr 2010 10:09:45 +0100 Christian Urban reorganised eqvt-file (now uses perm_simp already) file | diff | annotate
Wed, 28 Apr 2010 08:22:20 +0200 Christian Urban simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base file | diff | annotate
Tue, 27 Apr 2010 22:21:16 +0200 Christian Urban moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base file | diff | annotate
Mon, 26 Apr 2010 13:08:14 +0200 Christian Urban rewrote eqvts_raw to be a symtab, that can be looked up file | diff | annotate
Sun, 25 Apr 2010 09:13:16 +0200 Christian Urban tuned and cleaned file | diff | annotate
Thu, 22 Apr 2010 06:44:24 +0200 Christian Urban tuned parser file | diff | annotate
Thu, 22 Apr 2010 05:16:23 +0200 Christian Urban moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms file | diff | annotate
Sun, 18 Apr 2010 18:01:22 +0200 Christian Urban tuned file | diff | annotate
Sun, 18 Apr 2010 17:56:05 +0200 Christian Urban tuned file | diff | annotate
Sun, 18 Apr 2010 09:26:38 +0200 Christian Urban preliminary parser for perm_simp metod file | diff | annotate
Fri, 16 Apr 2010 16:29:11 +0200 Christian Urban automatic proofs for equivariance of alphas file | diff | annotate
Wed, 14 Apr 2010 16:05:58 +0200 Christian Urban tuned and removed dead code file | diff | annotate
Wed, 14 Apr 2010 14:41:54 +0200 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file file | diff | annotate
Wed, 14 Apr 2010 10:28:17 +0200 Christian Urban deleted test file | diff | annotate
Tue, 13 Apr 2010 00:47:57 +0200 Christian Urban moved equivariance of map into Nominal2_Eqvt file file | diff | annotate
Mon, 12 Apr 2010 13:34:54 +0200 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ file | diff | annotate
Sun, 11 Apr 2010 22:48:49 +0200 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ file | diff | annotate
Sun, 11 Apr 2010 18:08:57 +0200 Christian Urban used warning instead of tracing (does not seem to produce stable output) file | diff | annotate
Sun, 11 Apr 2010 10:36:09 +0200 Christian Urban added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed file | diff | annotate
Fri, 09 Apr 2010 21:51:01 +0200 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac file | diff | annotate
Sun, 04 Apr 2010 21:39:28 +0200 Christian Urban separated general nominal theory into separate folder file | diff | annotate | base
less more (0) tip
nominal2