src/HOL/Word/Word.thy
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Tue, 07 Dec 2010 14:53:44 +0100 boehmes moved smt_word.ML into the directory of the Word library
Tue, 30 Nov 2010 20:52:49 +0100 haftmann code preprocessor setup for numerals on word type;
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Wed, 18 Aug 2010 14:55:10 +0200 haftmann moved spurious auxiliary lemma here
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Thu, 01 Jul 2010 13:32:14 +0200 haftmann avoid bitstrings in generated code
Wed, 30 Jun 2010 17:12:38 +0200 haftmann one unified Word theory
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Mon, 08 Feb 2010 17:12:32 +0100 haftmann tuned spelling
Mon, 26 Jan 2009 22:14:16 +0100 haftmann entry point for Word library now named Word
less more (0) tip