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/Parser.thy
Wed, 17 Mar 2010 15:13:31 +0100 Christian Urban made paper to compile file | diff | annotate
Wed, 17 Mar 2010 12:18:35 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages. file | diff | annotate
Wed, 17 Mar 2010 08:39:46 +0100 Cezary Kaliszyk Lifting theorems with compound fv and compound alpha. file | diff | annotate
Tue, 16 Mar 2010 20:07:13 +0100 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. file | diff | annotate
Tue, 16 Mar 2010 15:27:47 +0100 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings. file | diff | annotate
Mon, 15 Mar 2010 17:42:17 +0100 Cezary Kaliszyk fv_eqvt_cheat no longer needed. file | diff | annotate
Mon, 15 Mar 2010 14:32:05 +0100 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster. file | diff | annotate
Mon, 15 Mar 2010 11:50:12 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work. file | diff | annotate
Mon, 15 Mar 2010 10:07:15 +0100 Cezary Kaliszyk explicit flag "cheat_equivp" file | diff | annotate
Sat, 13 Mar 2010 13:49:15 +0100 Christian Urban started supp-fv proofs (is going to work) file | diff | annotate
Fri, 12 Mar 2010 12:42:35 +0100 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let... file | diff | annotate
Thu, 11 Mar 2010 20:49:31 +0100 Cezary Kaliszyk Do not fail if the finite support proof fails. file | diff | annotate
Thu, 11 Mar 2010 19:41:11 +0100 Christian Urban support of atoms at the end of Abs.thy file | diff | annotate
Thu, 11 Mar 2010 17:47:29 +0100 Cezary Kaliszyk Show that the new types are in finite support typeclass. file | diff | annotate
Thu, 11 Mar 2010 15:11:57 +0100 Cezary Kaliszyk Remove "_raw" from lifted theorems. file | diff | annotate
Thu, 11 Mar 2010 14:05:36 +0100 Cezary Kaliszyk The cheats described explicitely. file | diff | annotate
Thu, 11 Mar 2010 13:34:45 +0100 Cezary Kaliszyk With the 4 cheats, all examples fully lift. file | diff | annotate
Thu, 11 Mar 2010 12:30:53 +0100 Cezary Kaliszyk Lift alpha_bn_constants. file | diff | annotate
Thu, 11 Mar 2010 12:26:24 +0100 Cezary Kaliszyk Lifting constants. file | diff | annotate
Thu, 11 Mar 2010 11:32:37 +0100 Cezary Kaliszyk Lifting constants works for all examples. file | diff | annotate
Thu, 11 Mar 2010 11:25:18 +0100 Cezary Kaliszyk Equivp working only on the standard alpha-equivalences. file | diff | annotate
Thu, 11 Mar 2010 11:20:50 +0100 Cezary Kaliszyk explicit cheat_fv_eqvt file | diff | annotate
Thu, 11 Mar 2010 11:15:14 +0100 Cezary Kaliszyk extract build_eqvts_tac. file | diff | annotate
Thu, 11 Mar 2010 10:39:29 +0100 Cezary Kaliszyk build_eqvts no longer requires permutations. file | diff | annotate
Thu, 11 Mar 2010 10:22:24 +0100 Cezary Kaliszyk Add explicit alpha_eqvt_cheat. file | diff | annotate
Thu, 11 Mar 2010 10:10:23 +0100 Cezary Kaliszyk Export tactic out of alpha_eqvt. file | diff | annotate
Wed, 10 Mar 2010 16:51:15 +0100 Christian Urban merged file | diff | annotate
Wed, 10 Mar 2010 16:50:42 +0100 Christian Urban almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining) file | diff | annotate
Wed, 10 Mar 2010 15:34:13 +0100 Cezary Kaliszyk Undoing mistakenly committed parser experiments. file | diff | annotate
Wed, 10 Mar 2010 15:32:51 +0100 Cezary Kaliszyk alpha_eqvt for recursive term1. file | diff | annotate
Wed, 10 Mar 2010 13:10:00 +0100 Cezary Kaliszyk Linked parser to fv and alpha. file | diff | annotate
Wed, 10 Mar 2010 12:48:38 +0100 Christian Urban parser produces ordered bn-fun information file | diff | annotate
Tue, 09 Mar 2010 22:08:38 +0100 Christian Urban added bn-information, but it is not yet ordered according to the dts file | diff | annotate
Tue, 09 Mar 2010 16:24:39 +0100 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings. file | diff | annotate
Mon, 08 Mar 2010 15:01:26 +0100 Christian Urban merged file | diff | annotate
Mon, 08 Mar 2010 15:01:01 +0100 Christian Urban updated to new Isabelle file | diff | annotate
Mon, 08 Mar 2010 11:12:15 +0100 Cezary Kaliszyk More fine-grained nominal restriction for debugging. file | diff | annotate
Fri, 05 Mar 2010 14:55:21 +0100 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt. file | diff | annotate
Thu, 04 Mar 2010 18:57:23 +0100 Cezary Kaliszyk Lift distinct. file | diff | annotate
Thu, 04 Mar 2010 15:55:53 +0100 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. file | diff | annotate
Thu, 04 Mar 2010 15:15:44 +0100 Cezary Kaliszyk Lift BV,FV,Permutations and injection :). file | diff | annotate
Thu, 04 Mar 2010 12:00:11 +0100 Cezary Kaliszyk Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials. file | diff | annotate
Wed, 03 Mar 2010 14:22:58 +0100 Cezary Kaliszyk Fix eqvt for multiple quantifiers. file | diff | annotate
Wed, 03 Mar 2010 11:42:15 +0100 Cezary Kaliszyk weird eqvt file | diff | annotate
Tue, 02 Mar 2010 21:43:27 +0100 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers. file | diff | annotate
Tue, 02 Mar 2010 17:48:41 +0100 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type. file | diff | annotate
Tue, 02 Mar 2010 15:11:41 +0100 Cezary Kaliszyk Working bv_eqvt file | diff | annotate
Tue, 02 Mar 2010 08:42:10 +0100 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser. file | diff | annotate
Tue, 02 Mar 2010 06:42:43 +0100 Christian Urban rawified the bind specs (ready to be used now) file | diff | annotate
Mon, 01 Mar 2010 19:23:08 +0100 Christian Urban modified for new binding format - hope it is the intended one file | diff | annotate
Mon, 01 Mar 2010 16:55:41 +0100 Christian Urban further code-refactoring in the parser file | diff | annotate
Mon, 01 Mar 2010 14:26:14 +0100 Christian Urban slight simplification of the raw-decl generation file | diff | annotate
Mon, 01 Mar 2010 07:46:50 +0100 Christian Urban added example from my phd file | diff | annotate
Sat, 27 Feb 2010 11:54:59 +0100 Christian Urban streamlined parser file | diff | annotate
Fri, 26 Feb 2010 18:38:25 +0100 Christian Urban generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders" file | diff | annotate
Thu, 25 Feb 2010 11:51:34 +0100 Christian Urban a few simplifications file | diff | annotate
Thu, 25 Feb 2010 08:40:52 +0100 Christian Urban added IsaMakefile...but so far included only a test for the parser file | diff | annotate | base
less more (0) tip
nominal2