isabelle: Changelog

huffman [Thu, 23 Aug 2007 23:34:51 +0200] rev 24416

avoid use of bin_rec_PM

huffman [Thu, 23 Aug 2007 20:15:45 +0200] rev 24415

new instance proofs

huffman [Thu, 23 Aug 2007 18:53:53 +0200] rev 24414

remove unused lemmas

huffman [Thu, 23 Aug 2007 18:52:44 +0200] rev 24413

import BinInduct; remove constant bin_rl; remove redundant lemmas and definitions; clean up some proofs

huffman [Thu, 23 Aug 2007 18:47:08 +0200] rev 24412

declare bin_rest_BIT_bin_last [simp]

huffman [Thu, 23 Aug 2007 16:47:16 +0200] rev 24411

Word/BinInduct.thy

huffman [Thu, 23 Aug 2007 16:46:40 +0200] rev 24410

theory of integers as an inductive datatype

huffman [Thu, 23 Aug 2007 15:47:42 +0200] rev 24409

move bin_nth stuff to its own subsection

huffman [Wed, 22 Aug 2007 21:09:21 +0200] rev 24408

removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type

huffman [Wed, 22 Aug 2007 20:59:19 +0200] rev 24407

typed print translation for CARD('a); declare zero_less_card_finite [simp]

isabelle