| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| Thu, 10 Sep 2015 14:12:22 +0200 |
wenzelm |
tuned -- avoid slightly odd @{cpat};
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
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
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 14:00:22 +0000 |
paulson |
fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
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
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:48 +0100 |
haftmann |
eliminated technical fact alias
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 11:18:36 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 02 Oct 2014 11:33:06 +0200 |
haftmann |
moved lemmas out of Int.thy which have nothing to do with int
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Fri, 30 May 2014 18:13:40 +0200 |
nipkow |
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:13:33 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
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, 12 Sep 2012 13:56:49 +0200 |
wenzelm |
standardized ML aliases;
|
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
|
| Tue, 17 Jan 2012 16:30:54 +0100 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 21:28:01 +0100 |
huffman |
use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|