Mon, 10 May 2010 14:11:50 +0200 |
haftmann |
one structure is better than three
|
file |
diff |
annotate
|
Mon, 10 May 2010 12:25:49 +0200 |
haftmann |
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
|
file |
diff |
annotate
|
Thu, 06 May 2010 19:27:51 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Thu, 06 May 2010 17:59:19 +0200 |
haftmann |
dropped duplicate comp_arith
|
file |
diff |
annotate
|
Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
Fri, 18 Sep 2009 09:07:50 +0200 |
haftmann |
tuned const_name antiquotations
|
file |
diff |
annotate
|
Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
Thu, 16 Apr 2009 14:02:13 +0200 |
haftmann |
added simproc
|
file |
diff |
annotate
|
Tue, 24 Mar 2009 13:13:18 +0100 |
nipkow |
fix
|
file |
diff |
annotate
|
Tue, 24 Mar 2009 12:45:01 +0100 |
nipkow |
presburger uses [arith] now
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
Fri, 20 Feb 2009 23:46:03 +0100 |
nipkow |
Removed redundant lemmas
|
file |
diff |
annotate
|
Tue, 17 Feb 2009 20:42:19 +0000 |
chaieb |
merged
|
file |
diff |
annotate
|
Tue, 17 Feb 2009 20:41:36 +0000 |
chaieb |
fixed selection of premises
|
file |
diff |
annotate
|
Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
Thu, 29 May 2008 23:46:40 +0200 |
wenzelm |
proper context for ss;
|
file |
diff |
annotate
|
Sat, 05 Jan 2008 23:05:29 +0100 |
chaieb |
Tuned relevant premises selection
|
file |
diff |
annotate
|
Thu, 03 Jan 2008 18:19:27 +0100 |
chaieb |
tuned relevance test for presburger
|
file |
diff |
annotate
|
Thu, 03 Jan 2008 10:27:34 +0100 |
chaieb |
Changed order of tactics in presburger --- thinning before case splits
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 15:14:24 +0100 |
haftmann |
some more antiquotations
|
file |
diff |
annotate
|
Fri, 12 Oct 2007 08:25:48 +0200 |
haftmann |
moved class power to theory Power
|
file |
diff |
annotate
|
Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
Wed, 22 Aug 2007 17:13:41 +0200 |
chaieb |
More selective generalization : a*b is generalized whenever none of a and b is a number
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:28:05 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
file |
diff |
annotate
|
Mon, 25 Jun 2007 22:46:55 +0200 |
wenzelm |
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
|
file |
diff |
annotate
|
Mon, 25 Jun 2007 00:36:37 +0200 |
wenzelm |
Thm.eta_long_conversion;
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 22:52:22 +0200 |
huffman |
add thm antiquotations
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|