| Sat, 27 Apr 2019 21:56:59 +0100 |
paulson |
tiny bit of extra restructuring
|
file |
diff |
annotate
|
| Wed, 24 Apr 2019 22:29:03 +0100 |
paulson |
getting rid of most apply steps
|
file |
diff |
annotate
|
| Tue, 15 May 2018 11:33:43 +0200 |
immler |
move FuncSet back to HOL-Library (amending 493b818e8e10)
|
file |
diff |
annotate
|
| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 16:11:24 +0100 |
wenzelm |
prefer context groups;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 16:01:52 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Sat, 26 Dec 2015 15:59:27 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 19:22:05 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:47:28 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
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
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 20:38:58 +0100 |
wenzelm |
recoded latin1 as utf8;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2009 20:59:12 +0200 |
nipkow |
tuned FuncSet
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 18:12:52 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 11:59:54 +0200 |
paulson |
simplified some steps
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:39:54 +0100 |
wenzelm |
fixed locale fact references;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Mar 2006 12:32:44 +0100 |
paulson |
Slight simplification of proofs
|
file |
diff |
annotate
|
| Mon, 23 Jan 2006 11:36:50 +0100 |
paulson |
fixed the <<= notation
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 10:22:13 +0100 |
paulson |
strengthened some lemmas; simplified some proofs
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 10:49:07 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 15 Apr 2004 14:17:45 +0200 |
nipkow |
Added ex/Exceptions.thy
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 18:52:26 +0200 |
wenzelm |
adapted locales;
|
file |
diff |
annotate
|
| Wed, 08 May 2002 09:08:16 +0200 |
paulson |
Tidied and converted to Isar by lcp
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 20:59:43 +0100 |
wenzelm |
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 22:34:11 +0200 |
wenzelm |
back again, supposedly with correct perms;
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 22:32:22 +0200 |
wenzelm |
fixed perms and final nl;
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:30:50 +0200 |
paulson |
HOL/ex/Tarski: new example by Florian Kammueller
|
file |
diff |
annotate
|