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/Ex/Lambda.thy
Sun, 29 Aug 2010 13:36:03 +0800 Christian Urban renamed NewParser to Nominal2 file | diff | annotate
Fri, 27 Aug 2010 13:57:00 +0800 Christian Urban make copies of the "old" files file | diff | annotate
Fri, 27 Aug 2010 03:37:17 +0800 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding) file | diff | annotate
Thu, 26 Aug 2010 02:08:00 +0800 Christian Urban cleaned up (almost completely) the examples file | diff | annotate
Wed, 25 Aug 2010 22:55:42 +0800 Christian Urban automatic lifting file | diff | annotate
Wed, 25 Aug 2010 11:58:37 +0800 Christian Urban now every lemma lifts (even with type variables) file | diff | annotate
Wed, 25 Aug 2010 09:02:06 +0800 Christian Urban can now deal with type variables in nominal datatype definitions file | diff | annotate
Sat, 21 Aug 2010 17:55:42 +0800 Christian Urban nominal_datatypes with type variables do not work file | diff | annotate
Sat, 21 Aug 2010 16:20:10 +0800 Christian Urban changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default file | diff | annotate
Mon, 07 Jun 2010 11:43:01 +0200 Christian Urban work on transitivity proof file | diff | annotate
Fri, 21 May 2010 17:17:51 +0200 Cezary Kaliszyk Match_Lam defined on Quotient Level. file | diff | annotate
Fri, 21 May 2010 11:55:22 +0200 Cezary Kaliszyk More on Function-defined subst. file | diff | annotate
Fri, 21 May 2010 10:47:45 +0200 Cezary Kaliszyk merge file | diff | annotate
Fri, 21 May 2010 10:43:14 +0200 Cezary Kaliszyk Renamings. file | diff | annotate
Fri, 21 May 2010 10:47:07 +0200 Cezary Kaliszyk merge (non-trival) file | diff | annotate
Fri, 21 May 2010 10:45:29 +0200 Cezary Kaliszyk Previously uncommited direct subst definition changes. file | diff | annotate
Fri, 21 May 2010 10:44:07 +0200 Cezary Kaliszyk Function experiments file | diff | annotate
Wed, 19 May 2010 12:29:08 +0200 Cezary Kaliszyk more subst experiments file | diff | annotate
Wed, 19 May 2010 11:29:42 +0200 Cezary Kaliszyk More subst experminets file | diff | annotate
Tue, 18 May 2010 17:56:41 +0200 Cezary Kaliszyk more on subst file | diff | annotate
Tue, 18 May 2010 17:17:54 +0200 Cezary Kaliszyk Single variable substitution file | diff | annotate
Tue, 18 May 2010 17:06:21 +0200 Cezary Kaliszyk subst fix file | diff | annotate
Tue, 18 May 2010 15:58:52 +0200 Cezary Kaliszyk subst experiments file | diff | annotate
Wed, 12 May 2010 16:59:53 +0100 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy file | diff | annotate
Tue, 11 May 2010 18:20:25 +0200 Cezary Kaliszyk Include raw permutation definitions in eqvt file | diff | annotate
Tue, 11 May 2010 17:16:57 +0200 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]' file | diff | annotate
Sun, 09 May 2010 12:26:10 +0100 Christian Urban cleaned up a bit the examples; added equivariance to all examples file | diff | annotate
Tue, 04 May 2010 11:22:22 +0200 Cezary Kaliszyk Move 2 more to NewParser file | diff | annotate
Mon, 26 Apr 2010 20:17:41 +0200 Christian Urban some changes to the paper file | diff | annotate
Mon, 26 Apr 2010 08:19:11 +0200 Christian Urban eliminated command so that all compiles file | diff | annotate
Mon, 26 Apr 2010 08:08:20 +0200 Christian Urban changed theorem_i to theorem....requires new Isabelle file | diff | annotate
Sun, 25 Apr 2010 09:13:16 +0200 Christian Urban tuned and cleaned file | diff | annotate
Fri, 16 Apr 2010 16:29:11 +0200 Christian Urban automatic proofs for equivariance of alphas file | diff | annotate
Fri, 16 Apr 2010 11:09:32 +0200 Cezary Kaliszyk Finished proof in Lambda.thy file | diff | annotate
Fri, 16 Apr 2010 10:46:50 +0200 Christian Urban attempt to manual prove eqvt for alpha file | diff | annotate
Fri, 16 Apr 2010 10:18:16 +0200 Christian Urban some tuning of eqvt-infrastructure file | diff | annotate
Wed, 14 Apr 2010 22:23:52 +0200 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell 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 13:21:11 +0200 Christian Urban first working version of the automatic equivariance procedure file | diff | annotate
Wed, 14 Apr 2010 10:29:34 +0200 Christian Urban preliminary tests file | diff | annotate
Tue, 13 Apr 2010 07:40:54 +0200 Christian Urban made everything to compile file | diff | annotate
Tue, 13 Apr 2010 00:53:32 +0200 Christian Urban some small tunings (incompleted work in Lambda.thy) file | diff | annotate
Mon, 12 Apr 2010 17:44:26 +0200 Christian Urban early ott paper 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:11:13 +0200 Christian Urban a few tests 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
Fri, 09 Apr 2010 11:08:05 +0200 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper file | diff | annotate | base
less more (0) tip
nominal2