src/HOL/Nominal/Examples/SN.thy
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.