| Sat, 16 Apr 2011 20:49:48 +0200 |
wenzelm |
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
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
|
| Fri, 23 Apr 2010 16:17:24 +0200 |
haftmann |
dequalified fact name
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 23:02:56 +0200 |
wenzelm |
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Mon, 25 May 2009 12:46:14 +0200 |
wenzelm |
proper signature constraints;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 08:34:51 +0200 |
haftmann |
added both cancel_div_mod_procs
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:53:09 +0100 |
wenzelm |
more regular method setup via SIMPLE_METHOD;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 10:58:18 +0100 |
hoelzl |
Updated paths in Decision_Procs comments and NEWS
|
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 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 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
| base
|