isabelle: Changelog

huffman [Wed, 30 Nov 2005 01:01:15 +0100] rev 18293

reimplement Case expression pattern matching to support lazy patterns

huffman [Wed, 30 Nov 2005 00:59:04 +0100] rev 18292

add definitions as defs, not axioms

huffman [Wed, 30 Nov 2005 00:56:01 +0100] rev 18291

changed section names

huffman [Wed, 30 Nov 2005 00:55:24 +0100] rev 18290

add xsymbol syntax for u type constructor

huffman [Wed, 30 Nov 2005 00:53:30 +0100] rev 18289

add constant unit_when

wenzelm [Wed, 30 Nov 2005 00:46:08 +0100] rev 18288

proper treatment of tuple/tuple_fun -- nest to the left!

wenzelm [Tue, 29 Nov 2005 23:00:20 +0100] rev 18287

moved nth_list to Pure/library.ML;

wenzelm [Tue, 29 Nov 2005 23:00:03 +0100] rev 18286

added nth_list;

wenzelm [Tue, 29 Nov 2005 22:52:19 +0100] rev 18285

added mk_split;

urbanc [Tue, 29 Nov 2005 19:26:38 +0100] rev 18284

changed the order of the induction variable and the context in lam_induct (test to see whether it simplifies the code for nominal_induct).

isabelle