nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 tip

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
simple cases for string rule inductions
2011-01-03, by Christian Urban
changed res keyword to set+ for restrictions; comment by a referee
2010-12-31, by Christian Urban
added proper case names for all induct and exhaust theorems
2010-12-31, by Christian Urban
added small example for strong inductions; functions still need a sorry
2010-12-31, by Christian Urban
removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-30, by Christian Urban
automated all strong induction lemmas
2010-12-28, by Christian Urban
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-28, by Christian Urban
generated goals for strong induction theorems.
2010-12-26, by Christian Urban
test with strong inductions
2010-12-23, by Christian Urban
moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23, by Christian Urban
moved generic functions into nominal_library
2010-12-23, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
tuned examples
2010-12-22, by Christian Urban
added fold_right which produces the correct term for left-infix operators
2010-12-22, by Christian Urban
updated to Isabelle 22 December
2010-12-22, by Christian Urban
a bit tuning
2010-12-22, by Christian Urban
corrected premises of strong exhausts theorems
2010-12-22, by Christian Urban

less more | (0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 tip

nominal2