Tue, 28 Oct 2008 11:03:07 +0100 | ballarin | Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'. | file | diff | annotate |
Mon, 29 Sep 2008 12:31:59 +0200 | haftmann | clarified dependencies between arith tools | file | diff | annotate |
Mon, 11 Aug 2008 14:50:02 +0200 | haftmann | re-arranged class dense_linear_order | file | diff | annotate |
Mon, 07 Jul 2008 08:47:17 +0200 | haftmann | absolute imports of HOL/*.thy theories | file | diff | annotate |
Thu, 26 Jun 2008 10:07:01 +0200 | haftmann | established Plain theory and image | file | diff | annotate |
Wed, 05 Mar 2008 21:24:03 +0100 | wenzelm | explicit referencing of background facts; | file | diff | annotate |
Wed, 27 Feb 2008 14:39:58 +0100 | chaieb | Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields. | file | diff | annotate |