| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +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, 29 Oct 2014 15:28:27 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 11:40:23 +0100 |
wenzelm |
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 16:25:33 +0100 |
wenzelm |
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:04:50 +0200 |
huffman |
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 20 May 2011 09:31:36 +0200 |
krauss |
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:33 +0100 |
haftmann |
meaningful transfer certificate
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 21:19:48 +0100 |
haftmann |
misc tuning
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:58 +0100 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 17:21:47 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 22:13:09 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:26:51 +0200 |
haftmann |
obey underscore naming convention
|
file |
diff |
annotate
| base
|