Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
2011-06-01 Cezary Kaliszyk DB translation using index; easier to reason about. file | diff | annotate
2011-06-01 Cezary Kaliszyk Problem: free variables in the goal file | diff | annotate
2011-06-01 Cezary Kaliszyk fixed previous commit file | diff | annotate
2011-06-01 Cezary Kaliszyk equivariance of db_trans file | diff | annotate
2011-05-31 Christian Urban fixed the problem with cps-like functions file | diff | annotate
2011-05-31 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way file | diff | annotate
2011-05-31 Cezary Kaliszyk map_term can be defined when equivariance is assumed file | diff | annotate
2011-05-31 Cezary Kaliszyk map_term is not a function the way it is defined file | diff | annotate
2011-05-31 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case. file | diff | annotate
2011-05-31 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity file | diff | annotate
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition file | diff | annotate
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier file | diff | annotate
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy) file | diff | annotate
2011-05-03 Christian Urban added two mutual recursive inductive definitions file | diff | annotate
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) file | diff | annotate
2011-04-18 Christian Urban merged file | diff | annotate
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April file | diff | annotate
2011-04-15 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs. file | diff | annotate
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive file | diff | annotate
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules. file | diff | annotate
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed file | diff | annotate
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions file | diff | annotate
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy file | diff | annotate
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases file | diff | annotate
2011-01-19 Christian Urban defined height as a function that returns an integer file | diff | annotate
2011-01-18 Christian Urban defined properly substitution file | diff | annotate
2011-01-18 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions file | diff | annotate
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) file | diff | annotate
2011-01-17 Christian Urban added a few examples of functions to Lambda.thy file | diff | annotate
2011-01-17 Christian Urban removed old testing code from Lambda.thy file | diff | annotate
2011-01-09 Christian Urban solved subgoals for depth and subst function file | diff | annotate
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions file | diff | annotate
2011-01-06 Christian Urban tuned file | diff | annotate
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee file | diff | annotate
2010-12-28 Christian Urban automated all strong induction lemmas file | diff | annotate
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples file | diff | annotate
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package file | diff | annotate
2010-09-29 Christian Urban simplified exhaust proofs file | diff | annotate
2010-09-29 Christian Urban test with induct_schema for simpler strong_ind proofs file | diff | annotate
2010-08-29 Christian Urban renamed NewParser to Nominal2 file | diff | annotate
2010-08-27 Christian Urban make copies of the "old" files file | diff | annotate
2010-08-26 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding) file | diff | annotate
2010-08-25 Christian Urban cleaned up (almost completely) the examples file | diff | annotate
2010-08-25 Christian Urban automatic lifting file | diff | annotate
2010-08-25 Christian Urban now every lemma lifts (even with type variables) file | diff | annotate
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions file | diff | annotate
2010-08-21 Christian Urban nominal_datatypes with type variables do not work file | diff | annotate
2010-08-21 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
2010-06-07 Christian Urban work on transitivity proof file | diff | annotate
2010-05-21 Cezary Kaliszyk Match_Lam defined on Quotient Level. file | diff | annotate
2010-05-21 Cezary Kaliszyk More on Function-defined subst. file | diff | annotate
2010-05-21 Cezary Kaliszyk merge file | diff | annotate
2010-05-21 Cezary Kaliszyk Renamings. file | diff | annotate
2010-05-21 Cezary Kaliszyk merge (non-trival) file | diff | annotate
2010-05-21 Cezary Kaliszyk Previously uncommited direct subst definition changes. file | diff | annotate
2010-05-21 Cezary Kaliszyk Function experiments file | diff | annotate
2010-05-19 Cezary Kaliszyk more subst experiments file | diff | annotate
2010-05-19 Cezary Kaliszyk More subst experminets file | diff | annotate
2010-05-18 Cezary Kaliszyk more on subst file | diff | annotate
2010-05-18 Cezary Kaliszyk Single variable substitution file | diff | annotate
less more (0) -60 tip
nominal2