| Mon, 28 Dec 2015 23:13:33 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 21:39:33 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 13:30:59 +0100 |
wenzelm |
support 'for' fixes in rule_tac etc.;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 14:48:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 22:30:57 +0100 |
wenzelm |
more position information;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 00:21:11 +0100 |
paulson |
tiny refinements
|
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
|
| Fri, 12 Apr 2013 17:02:55 +0200 |
wenzelm |
removed historic comments;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Fri, 12 Aug 2011 14:45:50 -0700 |
huffman |
make more HOL theories work with separate set type
|
file |
diff |
annotate
|
| Tue, 28 Jun 2011 12:47:32 +0100 |
paulson |
keyfree: The set of key-free messages (and associated theorems)
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 17:03:13 +0200 |
wenzelm |
simplified/modernized method setup;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 15:46:13 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 02 Feb 2011 14:11:26 +0000 |
paulson |
Introduction of metis calls and other cosmetic modifications.
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 13:25:32 +0100 |
paulson |
tidied using inductive_simps
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 17:08:41 +0000 |
paulson |
Simplified a couple of proofs and corrected a comment
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 21:33:25 +0100 |
wenzelm |
modernized syntax/translations;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 21:28:27 +0100 |
wenzelm |
modernized some syntax translations;
|
file |
diff |
annotate
|
| Thu, 24 Dec 2009 17:30:55 +0000 |
paulson |
tidied proofs
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
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
|
| Tue, 21 Jul 2009 11:09:50 +0200 |
haftmann |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|