src/HOL/Library/Code_Integer.thy
Mon, 23 Jul 2012 09:28:03 +0200 haftmann restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
Tue, 05 Jun 2012 07:10:51 +0200 haftmann prefer sys.error over plain error in Scala to avoid deprecation warning
Fri, 30 Mar 2012 11:16:35 +0200 huffman removed redundant nat-specific copies of theorems
Mon, 26 Mar 2012 19:04:17 +0200 huffman code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Thu, 26 Aug 2010 12:19:49 +0200 haftmann prevent line breaks after Scala symbolic operators
Wed, 28 Jul 2010 12:12:29 +0200 haftmann may use `int` in Isabelle runtime environment
Mon, 26 Jul 2010 11:10:35 +0200 haftmann added Code_Natural.thy
Sat, 24 Jul 2010 18:08:41 +0200 haftmann another refinement chapter in the neverending numeral story
Fri, 23 Jul 2010 10:58:13 +0200 haftmann avoid unreliable Haskell Int type
Fri, 22 Jan 2010 13:38:28 +0100 haftmann code literals: distinguish numeral classes by different entries
Thu, 14 Jan 2010 17:47:39 +0100 haftmann added Scala setup
Wed, 23 Sep 2009 14:00:12 +0200 haftmann Code_Eval(uation)
Tue, 02 Jun 2009 15:53:05 +0200 haftmann OCaml builtin intergers are elusive; avoid
Tue, 19 May 2009 16:54:55 +0200 haftmann String.literal replaces message_string, code_numeral replaces (code_)index
Tue, 19 May 2009 13:57:32 +0200 haftmann moved Code_Index, Random and Quickcheck before Main
Mon, 18 May 2009 15:45:34 +0200 haftmann added Code_Index.int_of operation
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Mon, 16 Feb 2009 19:11:15 +0100 haftmann added pdivmod on int (for code generation)
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Thu, 25 Sep 2008 09:28:03 +0200 haftmann discontinued special treatment of op = vs. eq_class.eq
Tue, 16 Sep 2008 09:21:24 +0200 haftmann evaluation using code generator
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Fri, 28 Mar 2008 22:01:01 +0100 haftmann accomodated to sledgehammer theory dependency requirement
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Tue, 29 Jan 2008 10:19:56 +0100 haftmann treating division by zero properly
Mon, 21 Jan 2008 08:43:27 +0100 haftmann tuned code setup
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Wed, 02 Jan 2008 15:14:23 +0100 haftmann index now a copy of nat rather than int
Fri, 12 Oct 2007 10:26:18 +0200 haftmann added
less more (0) tip