Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Fri, 19 Oct 2012 09:40:24 +0100 Christian Urban updated to changes in the type-def package changeset | files
Thu, 04 Oct 2012 12:44:43 +0100 Christian Urban removed "use" - replaced by "ML_file" changeset | files
Thu, 04 Oct 2012 11:10:23 +0100 Christian Urban removed fork_mono flag changeset | files
Tue, 28 Aug 2012 16:48:07 +0100 Christian Urban tuned changeset | files
Tue, 28 Aug 2012 16:47:26 +0100 Christian Urban added a nefangled ROOT file changeset | files
Tue, 07 Aug 2012 18:54:52 +0100 Christian Urban definition of an auxiliary graph in nominal-primrec definitions changeset | files
Tue, 07 Aug 2012 18:53:50 +0100 Christian Urban tuned changeset | files
Tue, 07 Aug 2012 16:55:17 +0100 Christian Urban added eqvt-lemma for function composition changeset | files
Mon, 06 Aug 2012 13:50:19 +0100 Christian Urban added new ROOT session file changeset | files
Fri, 03 Aug 2012 14:46:25 +0200 webertj command_spec antiquotation. changeset | files
Sun, 15 Jul 2012 13:03:47 +0100 Christian Urban added a simproc for alpha-equivalence to the simplifier changeset | files
Thu, 12 Jul 2012 10:11:32 +0100 Christian Urban streamlined definition of alpha-equivalence for single binders (used flip instead of swap) changeset | files
Mon, 18 Jun 2012 14:50:02 +0100 Christian Urban used ML-antiquotation command_spec for new commands changeset | files
Tue, 12 Jun 2012 14:22:58 +0100 Christian Urban added eqvt for finfun_apply changeset | files
Tue, 12 Jun 2012 13:56:16 +0100 Christian Urban improved the finfun parts changeset | files
Tue, 12 Jun 2012 01:23:52 +0100 Christian Urban added finfun-type to Nominal changeset | files
Mon, 11 Jun 2012 14:02:57 +0100 Christian Urban added CPS files to test (not all proofs have been completed) changeset | files
Sat, 09 Jun 2012 19:48:19 +0100 Christian Urban added a rule about inequality of freshness between atoms to the simplifier changeset | files
Wed, 06 Jun 2012 14:50:47 +0100 Christian Urban a simproc for simplifying Fresh when there is a sufficiently fresh atom changeset | files
Mon, 04 Jun 2012 21:39:51 +0100 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often changeset | files
Thu, 31 May 2012 12:01:13 +0100 Christian Urban merged changeset | files
Thu, 31 May 2012 12:01:01 +0100 Christian Urban added to the simplifier nominal_datatype.fresh lemmas changeset | files
Thu, 31 May 2012 11:59:56 +0100 Christian Urban added let-eqvt back changeset | files
Thu, 31 May 2012 12:44:37 +0200 Cezary Kaliszyk Propagare changes from Nominal2_Base to _Exec changeset | files
Thu, 31 May 2012 10:05:19 +0100 Christian Urban renamed fresh_fun to Fresh; added a simproc that deals with freshness of functions changeset | files
Mon, 28 May 2012 18:03:06 +0100 Christian Urban added library routines for the constant fresh changeset | files
Fri, 25 May 2012 15:46:48 +0100 Christian Urban fixed bug in simproc (also in the exec-version) changeset | files
Thu, 24 May 2012 10:17:32 +0200 Cezary Kaliszyk Synchronize Nominal2_Base_Exec with Nominal2_Base, equivariance for Let, avoid overloading approx twice and changes for new isabelle changeset | files
Wed, 23 May 2012 23:57:27 +0100 Christian Urban improved handling in the simplifier for inequalities derived from freshness assumptions changeset | files
Tue, 22 May 2012 14:55:58 +0200 Cezary Kaliszyk Executing Lambda Terms changeset | files
Tue, 22 May 2012 14:00:59 +0200 Cezary Kaliszyk Added workaround for broken quotient_type in tip isabelle. changeset | files
Sat, 12 May 2012 22:24:04 +0100 Christian Urban further cleaning Nominal2-Isabelle2012 changeset | files
Sat, 12 May 2012 22:21:25 +0100 Christian Urban cleaned also examples Nominal2-Isabelle2012 changeset | files
Sat, 12 May 2012 21:39:09 +0100 Christian Urban cleaned the repository for Nominal2-Isabelle2012 Nominal2-Isabelle2012 changeset | files
Sat, 12 May 2012 21:05:59 +0100 Christian Urban Created branch for Isabelle-2012 Nominal2-Isabelle2012 changeset | files
Sat, 12 May 2012 20:54:00 +0100 Christian Urban added a lemma about composition and permutations changeset | files
Tue, 01 May 2012 12:16:04 +0100 Christian Urban merged changeset | files
Mon, 30 Apr 2012 15:45:23 +0100 Christian Urban adapted to change by Markus on function.ML changeset | files
Fri, 20 Apr 2012 18:58:03 +0200 Cezary Kaliszyk Find remaining rsp theorems and provide them with the quotient definitions changeset | files
Fri, 20 Apr 2012 15:58:13 +0200 Cezary Kaliszyk Declare rsp for permute, permute_bn, alpha_bn together with their definitions instead of TrueI changeset | files
Fri, 20 Apr 2012 15:29:40 +0200 Cezary Kaliszyk merge changeset | files
Fri, 20 Apr 2012 15:28:35 +0200 Cezary Kaliszyk Pass proper rsp theorems for constructors and for size changeset | files
Thu, 19 Apr 2012 15:39:46 +0100 Christian Urban final changes to the lmcs-paper changeset | files
Thu, 12 Apr 2012 01:39:54 +0100 Christian Urban another iteration of the lmcs paper changeset | files
Tue, 10 Apr 2012 16:02:30 +0100 Christian Urban moved lift_raw_const from Quotient to Nominal changeset | files
Tue, 10 Apr 2012 15:22:16 +0100 Christian Urban updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore) changeset | files
Tue, 10 Apr 2012 15:21:07 +0100 Christian Urban slight polishing on Quotient paper changeset | files
Tue, 10 Apr 2012 15:19:42 +0100 Christian Urban ditto changeset | files
Tue, 10 Apr 2012 15:18:52 +0100 Christian Urban some slight polishing on the LMCS paper changeset | files
Wed, 04 Apr 2012 06:20:16 +0100 Christian Urban merged changeset | files
Wed, 04 Apr 2012 06:19:38 +0100 Christian Urban updated to Isabelle version April 1 changeset | files
Tue, 03 Apr 2012 23:09:13 +0100 Christian Urban a bit more on the qpaper changeset | files
Tue, 03 Apr 2012 16:38:56 +0200 Cezary Kaliszyk A recursive function over let-recs with eqvt problems changeset | files
Mon, 02 Apr 2012 19:52:17 +0200 Cezary Kaliszyk remove smt calls changeset | files
Fri, 30 Mar 2012 16:08:00 +0200 Cezary Kaliszyk More cleaning changeset | files
Fri, 30 Mar 2012 13:56:36 +0200 Cezary Kaliszyk Clean the proof of Aux changeset | files
Fri, 30 Mar 2012 13:39:15 +0200 Cezary Kaliszyk Finish all subgoals about Aux. changeset | files
Fri, 30 Mar 2012 09:11:30 +0200 Cezary Kaliszyk More on Aux changeset | files
Fri, 30 Mar 2012 07:36:43 +0200 Cezary Kaliszyk Close some of the obvious subgoals in Aux changeset | files
Fri, 30 Mar 2012 07:15:24 +0200 Cezary Kaliszyk Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof. changeset | files
(0) -3000 -1000 -300 -100 -60 tip
nominal2