Nominal/Ex/Lambda.thy
2011-06-01 Cezary Kaliszyk Problem: free variables in the goal
2011-06-01 Cezary Kaliszyk fixed previous commit
2011-06-01 Cezary Kaliszyk equivariance of db_trans
2011-05-31 Christian Urban fixed the problem with cps-like functions
2011-05-31 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way
2011-05-31 Cezary Kaliszyk map_term can be defined when equivariance is assumed
2011-05-31 Cezary Kaliszyk map_term is not a function the way it is defined
2011-05-31 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
2011-05-31 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy)
2011-05-03 Christian Urban added two mutual recursive inductive definitions
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
2011-04-18 Christian Urban merged
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
2011-04-15 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases
2011-01-19 Christian Urban defined height as a function that returns an integer
2011-01-18 Christian Urban defined properly substitution
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
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
2011-01-17 Christian Urban added a few examples of functions to Lambda.thy
2011-01-17 Christian Urban removed old testing code from Lambda.thy
2011-01-09 Christian Urban solved subgoals for depth and subst function
less more (0) -50 -30 tip