src/HOL/Complex/ex/MIR.thy
Mon, 14 Jul 2008 11:04:42 +0200 haftmann unified curried gcd, lcm, zgcd, zlcm
Thu, 03 Jul 2008 11:16:33 +0200 haftmann code antiquotation roaring ahead
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Sat, 17 May 2008 23:37:09 +0200 wenzelm avoid undeclared variables within proofs;
Sat, 17 May 2008 21:46:22 +0200 wenzelm avoid undeclared variables within proofs;
Wed, 02 Jan 2008 15:14:20 +0100 haftmann some more primrec
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Wed, 29 Aug 2007 14:21:19 +0200 chaieb fixed Proofs
Mon, 20 Aug 2007 18:07:49 +0200 haftmann renamed code_gen to export_code
Mon, 20 Aug 2007 11:18:18 +0200 nipkow removed allpairs
Mon, 13 Aug 2007 21:22:37 +0200 haftmann renamed keyword "to" to "module_name"
Thu, 26 Jul 2007 21:51:37 +0200 chaieb Updated proofs;
Thu, 26 Jul 2007 21:48:01 +0200 nipkow fixed broken proof
Thu, 19 Jul 2007 21:47:45 +0200 haftmann adapted to new code generator framework
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Thu, 21 Jun 2007 20:07:26 +0200 wenzelm tuned proofs -- avoid implicit prems;
Mon, 11 Jun 2007 11:06:11 +0200 chaieb tuned Proof and Document
Tue, 05 Jun 2007 20:44:12 +0200 chaieb Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
less more (0) tip