| Thu, 20 Oct 2022 12:57:06 +0100 |
paulson |
tidying of ugly legacy proofs
|
file |
diff |
annotate
|
| Fri, 14 Oct 2022 15:48:31 +0100 |
paulson |
Tidying of some very old proofs
|
file |
diff |
annotate
|
| Thu, 13 Oct 2022 15:38:32 +0100 |
paulson |
Elimination of the archaic ASCII syntax
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 21:39:33 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
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
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
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
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
use case_of_simps
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 21:19:39 +0100 |
wenzelm |
prefer high-level elim_format;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 02 Feb 2011 14:11:26 +0000 |
paulson |
Introduction of metis calls and other cosmetic modifications.
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 18:38:30 +0200 |
bulwahn |
renewing specifications in HOL-Auth
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
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
|
| Fri, 14 Aug 2009 17:26:11 +0100 |
paulson |
sledgehammer used to streamline protocol proofs
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:35 +0200 |
wenzelm |
eliminated OldGoals.inst;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:02:25 +0200 |
wenzelm |
OldGoals.inst;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 20:25:16 +0200 |
wenzelm |
tuned ML bindings (for multithreading);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:35 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 16:13:53 +0100 |
paulson |
a few more named lemmas
|
file |
diff |
annotate
|
| Wed, 26 Oct 2005 16:31:53 +0200 |
paulson |
tidied away duplicate thm
|
file |
diff |
annotate
|