| Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 19:53:49 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 17:25:36 +0200 |
wenzelm |
tuned -- avoid slightly odd @{cpat};
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 23:46:21 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 23:03:55 +0200 |
wenzelm |
tuned proofs -- less digits;
|
file |
diff |
annotate
|
| Sat, 20 Jun 2015 22:20:27 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 20 Jun 2015 16:31:44 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 22:39:34 +0100 |
wenzelm |
more standard module name;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 21:27:58 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 14:37:56 +0200 |
hoelzl |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:31:12 +0200 |
wenzelm |
prefer plain subscript;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 20:47:33 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:39:01 +0200 |
wenzelm |
added some ad-hoc namespace prefixes to avoid duplicate facts;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 20:54:48 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 20:07:48 +0100 |
nipkow |
Some cleaning up
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Tue, 25 May 2010 22:21:31 +0200 |
wenzelm |
moved ML files where they are actually used;
|
file |
diff |
annotate
|