src/HOL/Nominal/Examples/Crary.thy
Fri, 20 Sep 2024 19:51:08 +0200 wenzelm standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
Wed, 24 Apr 2024 20:56:26 +0100 paulson More tidying of proofs
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Wed, 05 Sep 2012 20:19:37 +0200 wenzelm tuned proofs;
Mon, 21 Feb 2011 17:43:23 +0100 wenzelm modernized specifications;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 21 Sep 2009 15:02:23 +0200 Christian Urban tuned some proofs
Sat, 13 Dec 2008 13:24:45 +0100 berghofe Modified nominal_primrec to make it work with local theories, unified syntax
Thu, 28 Aug 2008 17:54:18 +0200 krauss more function -> fun
Thu, 22 May 2008 16:34:41 +0200 urbanc made the naming of the induction principles consistent: weak_induct is
Wed, 16 Apr 2008 02:25:06 +0200 urbanc removed test artefacts
less more (0) -15 tip