Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-120
+120
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
typo
2011-04-09, by Christian Urban
more on paper
2011-04-08, by Christian Urban
eqvt_lambda without eta-expansion
2011-04-08, by Christian Urban
changed default preprocessor that does not catch variables only occuring on the right
2011-04-06, by Christian Urban
final version of slides
2011-03-31, by Christian Urban
more on the slides
2011-03-30, by Christian Urban
tuned IsaMakefile
2011-03-30, by Christian Urban
rearranged directories and updated to new Isabelle
2011-03-29, by Christian Urban
precise path to LaTeXsugar
2011-03-16, by Christian Urban
a lit bit more on the pearl-jv paper
2011-03-16, by Christian Urban
ported changes from function package....needs Isabelle 16 March or above
2011-03-16, by Christian Urban
more on the pearl paper
2011-03-15, by Christian Urban
equivariance for All and Ex can be proved in terms of their definition
2011-03-14, by Christian Urban
more on the paper
2011-03-11, by Christian Urban
merged
2011-03-08, by Christian Urban
more on the pearl paper
2011-03-08, by Christian Urban
distinct names at toplevel
2011-03-02, by Cezary Kaliszyk
merge
2011-03-02, by Cezary Kaliszyk
Pairing function
2011-03-02, by Cezary Kaliszyk
updated pearl papers
2011-03-02, by Christian Urban
a bit more tuning
2011-03-01, by Christian Urban
included old test cases for perm_simp into ROOT.ML file
2011-02-28, by Christian Urban
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-02-28, by Christian Urban
some slight polishing
2011-02-25, by Christian Urban
merged
2011-02-24, by Christian Urban
added a lemma about fresh_star and Abs
2011-02-24, by Christian Urban
Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
2011-02-23, by Cezary Kaliszyk
typeschemes/subst
2011-02-19, by Cezary Kaliszyk
further experiments with typeschemes subst
2011-02-17, by Cezary Kaliszyk
Finished the proof of a function that invents fresh variable names.
2011-02-17, by Cezary Kaliszyk
added eqvt for length
2011-02-16, by Christian Urban
added eqvt lemmas for filter and distinct
2011-02-16, by Christian Urban
added eqvt for cartesian products
2011-02-07, by Christian Urban
cleaned up the experiments so that the tests go through
2011-02-07, by Christian Urban
merge
2011-02-05, by Cezary Kaliszyk
Experiments defining a function on Let
2011-02-05, by Cezary Kaliszyk
updated TODO
2011-02-04, by Christian Urban
Lambda.thy which works with Nominal_Isabelle2011
2011-02-04, by Christian Urban
merged
2011-02-03, by Christian Urban
removed diagnostic code
2011-02-03, by Christian Urban
Only one of the subgoals is needed
2011-02-01, by Cezary Kaliszyk
Experiments with substitution on set+
2011-02-01, by Cezary Kaliszyk
More properties that relate abs_res and abs_set. Also abs_res with less binders.
2011-02-01, by Cezary Kaliszyk
alpha_res implies alpha_set :)
2011-01-30, by Cezary Kaliszyk
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
2011-01-30, by Cezary Kaliszyk
Experiments with functions
2011-01-29, by Cezary Kaliszyk
some experiments
2011-01-27, by Christian Urban
the proofs with eqvt_at
2011-01-27, by Christian Urban
made eqvt-proof explicit in the function definitions
2011-01-25, by Christian Urban
merge
2011-01-25, by Cezary Kaliszyk
minor
2011-01-25, by Cezary Kaliszyk
Down as infixr
2011-01-25, by Cezary Kaliszyk
added some slides
2011-01-22, by Christian Urban
added Tutorial6
2011-01-23, by Christian Urban
cleaning up
2011-01-22, by Christian Urban
merged
2011-01-22, by Christian Urban
cleaned up Tutorial 3 with solutions
2011-01-22, by Christian Urban
Missing val.simps
2011-01-23, by Cezary Kaliszyk
merge
2011-01-23, by Cezary Kaliszyk
Tutorial 4s
2011-01-23, by Cezary Kaliszyk
cleaned up and solution section
2011-01-22, by Christian Urban
cleaned up tutorial1...added solution file
2011-01-22, by Christian Urban
better version of Tutorial 1
2011-01-22, by Christian Urban
better flow of proofs and definitions and proof
2011-01-21, by Christian Urban
separated type preservation and progress into a separate file
2011-01-21, by Christian Urban
substitution lemma in separate file
2011-01-21, by Christian Urban
added unbind example
2011-01-21, by Christian Urban
a bit tuning
2011-01-21, by Christian Urban
first split of tutorrial theory
2011-01-20, by Christian Urban
added a very rough version of the tutorial; all seems to work
2011-01-19, by Christian Urban
added obtain_fresh lemma; tuned Lambda.thy
2011-01-19, by Christian Urban
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
2011-01-19, by Christian Urban
ported some of the old proofs to serve as testcases
2011-01-19, by Christian Urban
added eqvt and supp lemma for removeAll (function from List.thy)
2011-01-19, by Christian Urban
theory name as it should be
2011-01-19, by Christian Urban
removed diagnostic code
2011-01-19, by Christian Urban
added Minimal file to test things
2011-01-19, by Christian Urban
defined height as a function that returns an integer
2011-01-19, by Christian Urban
deleted diagnostic code
2011-01-18, by Christian Urban
some tryes about substitution over type-schemes
2011-01-18, by Christian Urban
defined properly substitution
2011-01-18, by Christian Urban
derived stronger Abs_eq_iff2 theorems
2011-01-18, by Christian Urban
made alpha_abs_set_stronger1 stronger
2011-01-18, by Christian Urban
removed finiteness assumption from set_rename_perm
2011-01-18, by Christian Urban
alpha_abs_set_stronger1
2011-01-18, by Cezary Kaliszyk
alpha_abs_let_stronger is not true in the same form
2011-01-18, by Cezary Kaliszyk
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-18, by Christian Urban
modified the renaming_perm lemmas
2011-01-18, by Christian Urban
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
2011-01-17, by Christian Urban
added a few examples of functions to Lambda.thy
2011-01-17, by Christian Urban
exported nominal function code to external file
2011-01-17, by Christian Urban
removed old testing code from Lambda.thy
2011-01-17, by Christian Urban
moved high level code from LamTest into the main libraries.
2011-01-17, by Christian Urban
eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation
2011-01-17, by Christian Urban
subst also works now
2011-01-15, by Christian Urban
nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions
2011-01-15, by Christian Urban
strengthened renaming lemmas
2011-01-14, by Christian Urban
added eqvt_lemmas for subset and psubset
2011-01-13, by Christian Urban
a few lemmas about freshness for at and at_base
2011-01-10, by Christian Urban
added a property about finite support in the presense of eqvt_at
2011-01-10, by Christian Urban
instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis
2011-01-09, by Christian Urban
solved subgoals for depth and subst function
2011-01-09, by Christian Urban
added eqvt_at premises in function definition - however not proved at the moment
2011-01-09, by Christian Urban
added one further lemma about equivariance of THE_default
2011-01-07, by Christian Urban
equivariance of THE_default under the uniqueness assumption
2011-01-07, by Christian Urban
derived equivariance for the function graph and function relation
2011-01-07, by Christian Urban
a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06, by Christian Urban
removed last traces of debugging code
2011-01-06, by Christian Urban
removed debugging code abd introduced a guarded tracing function
2011-01-06, by Christian Urban
moved Weakening up....it does not compile when put at the last position
2011-01-06, by Christian Urban
tuned
2011-01-06, by Christian Urban
added weakening to the test cases
2011-01-06, by Christian Urban
cleaned up weakening proof and added a version with finit sets
2011-01-06, by Christian Urban
same
2011-01-06, by Christian Urban
some further lemmas for fsets
2011-01-06, by Christian Urban
made sure the raw datatypes and raw functions do not get any mixfix syntax
2011-01-06, by Christian Urban
exported the code into a separate file
2011-01-05, by Christian Urban
strong rule inductions; as an example the weakening lemma works
2011-01-05, by Christian Urban
final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-04, by Christian Urban
file with most of the strong rule induction development
2011-01-03, by Christian Urban
less
more
|
(0)
-1000
-120
+120
tip