Nominal/Ex/SingleLet.thy
Tue, 05 Jul 2011 18:42:34 +0200 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Fri, 31 Dec 2010 15:37:04 +0000 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
Wed, 22 Dec 2010 21:13:44 +0000 Christian Urban tuned examples
Tue, 21 Dec 2010 10:28:08 +0000 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Sat, 13 Nov 2010 22:23:26 +0000 Christian Urban lifted permute_bn constants
Fri, 12 Nov 2010 01:20:53 +0000 Christian Urban automated permute_bn functions (raw ones first)
Wed, 10 Nov 2010 13:46:21 +0000 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
Thu, 14 Oct 2010 04:14:22 +0100 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Tue, 05 Oct 2010 07:30:37 +0100 Christian Urban llncs and more sqeezing
Mon, 27 Sep 2010 12:19:17 -0400 Christian Urban added postprocessed fresh-lemmas for constructors
Mon, 27 Sep 2010 09:51:15 -0400 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
Mon, 27 Sep 2010 04:56:28 -0400 Christian Urban some experiments
Sat, 25 Sep 2010 08:38:04 -0400 Christian Urban lifted size_thms and exported them as <name>.size
Sat, 25 Sep 2010 08:28:45 -0400 Christian Urban cleaned up two examples
Sat, 18 Sep 2010 06:09:43 +0800 Christian Urban updated to Isabelle Sept 16
less more (0) -15 tip