| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 15:49:56 +0100 |
wenzelm |
proper ML expressions, without trailing semicolons;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 24 May 2018 09:26:26 +0000 |
haftmann |
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
replaced recdef were easy to replace
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 16:47:25 +0200 |
nipkow |
reorganized and added log-related lemmas
|
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, 20 Jun 2017 08:01:56 +0200 |
haftmann |
replaced recdef by fun
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 15:44:53 +0200 |
nipkow |
fixed floor proof
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:55 +0100 |
haftmann |
consolidated name
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 15:59:40 +0000 |
paulson |
MIR decision procedure again working
|
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
|
| Tue, 10 Nov 2015 14:43:29 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 20 Jun 2015 16:31:44 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 11:46:03 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 22:37:14 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
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 |
ported Decision_Procs to new datatypes
|
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
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 17:58:25 +0100 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 07 Mar 2013 17:50:26 +0100 |
wenzelm |
tuned proofs -- more structure, less warnings;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 15:59:18 +0100 |
wenzelm |
eliminated slightly odd identifiers;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 13:22:29 +0100 |
wenzelm |
eliminated some improper identifiers;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Mon, 03 Sep 2012 09:15:40 +0200 |
wenzelm |
some parallel ML;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|