src/HOL/Library/ExecutableRat.thy
Tue, 16 Jan 2007 08:06:55 +0100 haftmann refined and added example for ExecutableRat
Wed, 27 Dec 2006 19:10:00 +0100 haftmann added OCaml code generation (without dictionaries)
Mon, 27 Nov 2006 13:42:30 +0100 haftmann adjusted syntax for internal code generation
Wed, 22 Nov 2006 10:20:12 +0100 haftmann dropped eq const
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Mon, 06 Nov 2006 16:28:31 +0100 haftmann code generator module naming improved
Tue, 31 Oct 2006 14:58:12 +0100 haftmann adapted to new serializer syntax
Tue, 31 Oct 2006 09:29:01 +0100 haftmann dropped junk
Mon, 16 Oct 2006 14:07:31 +0200 haftmann moved HOL code generator setup to Code_Generator
Tue, 10 Oct 2006 09:17:20 +0200 haftmann added code_abstype
Tue, 26 Sep 2006 13:34:16 +0200 haftmann renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
Mon, 25 Sep 2006 17:04:18 +0200 haftmann better handling for div by zero
Tue, 19 Sep 2006 15:22:05 +0200 haftmann code generation 2 adjustments
Fri, 01 Sep 2006 08:36:51 +0200 haftmann final syntax for some Isar code generator keywords
Wed, 14 Jun 2006 12:14:13 +0200 haftmann slight adaptions for code generator
Tue, 06 Jun 2006 15:02:55 +0200 haftmann refined code generation
Thu, 11 May 2006 10:25:55 +0200 haftmann fixed codegen bug, cleanup
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Sat, 25 Feb 2006 15:19:19 +0100 haftmann change in codegen syntax
Thu, 16 Feb 2006 18:59:39 +0100 haftmann removed silly stuff
Tue, 14 Feb 2006 17:07:48 +0100 haftmann added theory of executable rational numbers
less more (0) tip