isabelle: Changelog

huffman [Fri, 22 Sep 2006 23:19:45 +0200] rev 20685

added lemmas about LIMSEQ and norm; simplified some proofs

huffman [Fri, 22 Sep 2006 23:17:39 +0200] rev 20684

add lemma norm_power

wenzelm [Fri, 22 Sep 2006 21:42:12 +0200] rev 20683

added HOL-Complex-ex;

huffman [Fri, 22 Sep 2006 16:25:15 +0200] rev 20682

define constants with THE instead of SOME

berghofe [Fri, 22 Sep 2006 14:36:23 +0200] rev 20681

Fixed bug concerning the generation of identifiers for datatypes, which caused the code generator to fail for mutually recursive datatypes.

berghofe [Fri, 22 Sep 2006 14:32:46 +0200] rev 20680

Replaced irreducible_paths by all_paths.

berghofe [Fri, 22 Sep 2006 14:30:37 +0200] rev 20679

Added function all_paths (formerly find_paths).

wenzelm [Fri, 22 Sep 2006 13:04:30 +0200] rev 20678

tuned proofs;

wenzelm [Thu, 21 Sep 2006 19:06:16 +0200] rev 20677

tuned oracle name;

wenzelm [Thu, 21 Sep 2006 19:06:03 +0200] rev 20676

added is_ml_reserved;

isabelle