| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 22:46:21 +0200 |
wenzelm |
prefer plain simpset operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 11:11:49 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:43 +0200 |
krauss |
removed complicated (and rarely helpful) error reporting
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:40 +0200 |
krauss |
discontinued continuations to simplify control flow; dropped optimization in scnp
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:38 +0200 |
krauss |
use Cache structure instead of passing tables around explicitly
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 17:01:12 +0200 |
wenzelm |
theory data merge: prefer left side uniformly;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:52:04 +0200 |
krauss |
default termination prover as plain tactic
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
file |
diff |
annotate
|
| Mon, 23 Nov 2009 15:05:59 +0100 |
krauss |
eliminated dead code and some unused bindings, reported by polyml
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 13:54:00 +0100 |
blanchet |
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:58:36 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 15:16:54 +0100 |
blanchet |
make "sizechange_tac" slightly less verbose
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 13:36:46 +0100 |
krauss |
renamed method sizechange to size_change
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 01:32:06 +0100 |
krauss |
less verbose termination tactics
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 21:28:39 +0200 |
wenzelm |
normalized aliases of Output operations;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|