Fri, 12 Dec 2008 20:03:30 +0100 |
ballarin |
Porting to new locales.
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
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
|