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.
Quot/Nominal/Terms.thy
2010-02-24 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5 file | diff | annotate
2010-02-24 Cezary Kaliszyk Define lifted perms. file | diff | annotate
2010-02-24 Cezary Kaliszyk With permute_rsp we can lift the instance proofs :). file | diff | annotate
2010-02-24 Cezary Kaliszyk Regularize finite support proof for trm1 file | diff | annotate
2010-02-23 Cezary Kaliszyk rsp for bv; the only issue is that it requires an appropriate induction principle. file | diff | annotate
2010-02-23 Cezary Kaliszyk rsp infrastructure. file | diff | annotate
2010-02-23 Cezary Kaliszyk Progress towards automatic rsp of constants and fv. file | diff | annotate
2010-02-23 Cezary Kaliszyk Looking at proving the rsp rules automatically. file | diff | annotate
2010-02-23 Cezary Kaliszyk Define the quotient from ML file | diff | annotate
2010-02-23 Cezary Kaliszyk Fixes for auxiliary datatypes. file | diff | annotate
2010-02-22 Cezary Kaliszyk Fixed pseudo_injectivity for trm4 file | diff | annotate
2010-02-22 Cezary Kaliszyk Testing auto equivp code. file | diff | annotate
2010-02-22 Cezary Kaliszyk A tactic for final equivp file | diff | annotate
2010-02-22 Cezary Kaliszyk More equivp infrastructure. file | diff | annotate
2010-02-22 Cezary Kaliszyk tactify transp file | diff | annotate
2010-02-22 Cezary Kaliszyk export the reflp and symp tacs. file | diff | annotate
2010-02-22 Cezary Kaliszyk Generalize atom_trans and atom_sym. file | diff | annotate
2010-02-22 Cezary Kaliszyk Some progress about transp file | diff | annotate
2010-02-22 Cezary Kaliszyk alpha-symmetric addons. file | diff | annotate
2010-02-22 Cezary Kaliszyk alpha reflexivity file | diff | annotate
2010-02-22 Cezary Kaliszyk Renaming. file | diff | annotate
2010-02-22 Cezary Kaliszyk Added missing description. file | diff | annotate
2010-02-21 Cezary Kaliszyk Removed bindings 'in itself' where possible. file | diff | annotate
2010-02-20 Cezary Kaliszyk Some adaptation file | diff | annotate
2010-02-19 Cezary Kaliszyk proof cleaning and standardizing. file | diff | annotate
2010-02-19 Cezary Kaliszyk Automatic production and proving of pseudo-injectivity. file | diff | annotate
2010-02-19 Cezary Kaliszyk Experiments for the pseudo-injectivity tactic. file | diff | annotate
2010-02-19 Cezary Kaliszyk merge file | diff | annotate
2010-02-19 Cezary Kaliszyk Constructing alpha_inj goal. file | diff | annotate
2010-02-18 Christian Urban merged file | diff | annotate
2010-02-18 Cezary Kaliszyk Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct. file | diff | annotate
2010-02-18 Cezary Kaliszyk Testing auto constant lifting. file | diff | annotate
2010-02-18 Cezary Kaliszyk Changed back to original version of trm5 file | diff | annotate
2010-02-18 Cezary Kaliszyk The alternate version of trm5 with additional binding. All proofs work the same. file | diff | annotate
2010-02-18 Cezary Kaliszyk Code for handling atom sets. file | diff | annotate
2010-02-18 Cezary Kaliszyk Replace Terms by Terms2. file | diff | annotate | base
2010-02-18 Cezary Kaliszyk Fixed proofs in Terms2 and found a mistake in Terms. file | diff | annotate
2010-02-17 Cezary Kaliszyk Cleaning of proofs in Terms. file | diff | annotate
2010-02-17 Cezary Kaliszyk Testing Fv file | diff | annotate
2010-02-17 Cezary Kaliszyk Fix the strong induction principle. file | diff | annotate
2010-02-17 Cezary Kaliszyk Tested the Perm code; works everywhere in Terms. file | diff | annotate
2010-02-12 Cezary Kaliszyk renamed 'as' to 'is' everywhere. file | diff | annotate
2010-02-11 Cezary Kaliszyk the lam/bla example. file | diff | annotate
2010-02-11 Cezary Kaliszyk Finished a working foo/bar. file | diff | annotate
2010-02-11 Cezary Kaliszyk fv_foo is not regular. file | diff | annotate
2010-02-11 Cezary Kaliszyk Testing foo/bar file | diff | annotate
2010-02-11 Cezary Kaliszyk Even when bv = fv it still doesn't lift. file | diff | annotate
2010-02-11 Cezary Kaliszyk Notation available locally file | diff | annotate
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2. file | diff | annotate
2010-02-10 Cezary Kaliszyk example with a respectful bn function defined over the type itself file | diff | annotate
2010-02-10 Cezary Kaliszyk Another mistake found with OTT. file | diff | annotate
2010-02-10 Cezary Kaliszyk Fixed rbv6, when translating to OTT. file | diff | annotate
2010-02-10 Cezary Kaliszyk A concrete example, with a proof that rbv is not regular and file | diff | annotate
2010-02-09 Christian Urban merged file | diff | annotate
2010-02-09 Christian Urban slight correction file | diff | annotate
2010-02-09 Cezary Kaliszyk merge file | diff | annotate
2010-02-09 Cezary Kaliszyk More about trm6 file | diff | annotate
2010-02-09 Christian Urban merged file | diff | annotate
2010-02-09 Cezary Kaliszyk the specifications of the respects. file | diff | annotate
2010-02-09 Cezary Kaliszyk trm6 with the 'Foo' constructor. file | diff | annotate
2010-02-09 Cezary Kaliszyk Explicitly marked what is bound. file | diff | annotate
2010-02-09 Cezary Kaliszyk Cleaning and updating in Terms. file | diff | annotate
2010-02-09 Cezary Kaliszyk Looking at the trm2 example file | diff | annotate
2010-02-08 Cezary Kaliszyk Proper context fixes lifting inside instantiations. file | diff | annotate
2010-02-05 Cezary Kaliszyk Cleaned Terms using [lifted] and found a workaround for the instantiation problem. file | diff | annotate
2010-02-03 Cezary Kaliszyk More let-rec experiments file | diff | annotate
2010-02-03 Christian Urban proposal for an alpha equivalence file | diff | annotate
2010-02-03 Cezary Kaliszyk Lets different. file | diff | annotate
2010-02-03 Cezary Kaliszyk Simplified the proof. file | diff | annotate
2010-02-03 Christian Urban merged file | diff | annotate
2010-02-03 Christian Urban proved that bv for lists respects alpha for terms file | diff | annotate
2010-02-03 Cezary Kaliszyk Finished remains on the let proof. file | diff | annotate
2010-02-03 Cezary Kaliszyk merge file | diff | annotate
2010-02-03 Cezary Kaliszyk Lets are ok. file | diff | annotate
2010-02-03 Christian Urban merged file | diff | annotate
2010-02-03 Christian Urban added type-scheme example file | diff | annotate
2010-02-03 Cezary Kaliszyk Definitions for trm5 file | diff | annotate
2010-02-03 Christian Urban merged file | diff | annotate
2010-02-03 Christian Urban fixed proofs that broke because of eqvt file | diff | annotate
2010-02-03 Cezary Kaliszyk Minor fix. file | diff | annotate
2010-02-03 Cezary Kaliszyk merge file | diff | annotate
2010-02-03 Cezary Kaliszyk alpha5 pseudo-injective file | diff | annotate
2010-02-03 Christian Urban fixed proofs in Abs.thy file | diff | annotate
2010-02-03 Cezary Kaliszyk The alpha-equivalence relation for let-rec. Not sure if correct... file | diff | annotate
2010-02-03 Cezary Kaliszyk Starting with a let-rec example. file | diff | annotate
2010-02-03 Cezary Kaliszyk Some cleaning and eqvt proof file | diff | annotate
2010-02-03 Cezary Kaliszyk The trm1_support lemma explicitly and stated a strong induction principle. file | diff | annotate
2010-02-03 Cezary Kaliszyk More ingredients in Terms. file | diff | annotate
2010-02-02 Cezary Kaliszyk Finished the supp_fv proof; first proof that analyses the structure of 'Let' :) file | diff | annotate
2010-02-02 Cezary Kaliszyk More in Terms file | diff | annotate
2010-02-02 Cezary Kaliszyk First experiments in Terms. file | diff | annotate
2010-01-28 Christian Urban minor file | diff | annotate
2010-01-27 Christian Urban completely ported file | diff | annotate
2010-01-27 Christian Urban mostly ported Terms.thy to new Nominal file | diff | annotate
2010-01-27 Christian Urban added Terms to Nominal - Instantiation of two types does not work (ask Florian) file | diff | annotate
less more (0) tip
nominal2