Nominal/Ex/SingleLet.thy
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-22 Christian Urban tuned examples
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-11-13 Christian Urban lifted permute_bn constants
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-10-14 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
2010-10-05 Christian Urban llncs and more sqeezing
2010-09-27 Christian Urban added postprocessed fresh-lemmas for constructors
2010-09-27 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
2010-09-27 Christian Urban some experiments
2010-09-25 Christian Urban lifted size_thms and exported them as <name>.size
2010-09-25 Christian Urban cleaned up two examples
2010-09-17 Christian Urban updated to Isabelle Sept 16
less more (0) -15 tip