src/HOL/Nominal/Examples/SN.thy
2006-07-02 urbanc 2006-07-02 added more infrastructure for the recursion combinator
2006-05-20 wenzelm 2006-05-20 primrec (unchecked);
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-04-28 berghofe 2006-04-28 Capitalized theory names.
2006-03-08 urbanc 2006-03-08 deleted some proofs "on comment"
2006-01-11 urbanc 2006-01-11 changes to make use of the new induction principle proved by Stefan horay (hooraayyy)
2006-01-11 urbanc 2006-01-11 tuned proofs
2006-01-07 urbanc 2006-01-07 another change for the new induct-method
2006-01-07 urbanc 2006-01-07 changed PRO_RED proof to conform with the new induction rules
2005-12-11 urbanc 2005-12-11 ISAR-fied some proofs
2005-12-11 urbanc 2005-12-11 completed the sn proof and changed the manual accordingly
2005-12-09 urbanc 2005-12-09 tuned
2005-12-04 urbanc 2005-12-04 tuned
2005-12-04 urbanc 2005-12-04 added an Isar-proof for the abs_ALL lemma
2005-12-01 urbanc 2005-12-01 initial cleanup to use the new induction method
2005-11-28 urbanc 2005-11-28 some small tuning
2005-11-27 urbanc 2005-11-27 cleaned up all examples so that they work with the current nominal-setting.
2005-11-07 urbanc 2005-11-07 Initial commit.