| Sun, 29 Mar 2020 21:30:52 +0100 |
paulson |
more ugly old proofs
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Tue, 24 Sep 2019 12:56:10 +0100 |
paulson |
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
|
file |
diff |
annotate
|
| 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
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:20 +0000 |
haftmann |
replaced some ancient ASCII syntax
|
file |
diff |
annotate
|
| Thu, 12 Jul 2018 17:22:39 +0100 |
paulson |
de-applying (mostly Set_Interval)
|
file |
diff |
annotate
|
| Sat, 16 Jun 2018 22:09:24 +0200 |
nipkow |
more simp
|
file |
diff |
annotate
|
| Sat, 16 Jun 2018 20:32:00 +0200 |
nipkow |
moved lemmas from AFP
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 19:19:11 +0100 |
wenzelm |
more abbrevs;
|
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
|
| Fri, 05 Aug 2016 18:14:28 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2016 20:19:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 13:49:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 12:39:51 +0100 |
wenzelm |
option "inductive_defs" controls exposure of def and mono facts;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 07 Jul 2015 18:01:30 +0200 |
hoelzl |
add monotonicity rule for rtranclp
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 22 Jun 2014 12:37:55 +0200 |
nipkow |
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
|
file |
diff |
annotate
|
| Sat, 21 Jun 2014 15:46:52 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Fri, 06 Jun 2014 10:53:33 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 21:40:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:53 +0100 |
hoelzl |
add acyclicI_order
|
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
|
| Sun, 23 Dec 2012 19:54:15 +0100 |
nipkow |
renamed and added lemmas
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 17:22:51 +0200 |
Christian Sternagel |
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 09:04:29 +0200 |
haftmann |
power on predicate relations
|
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
|
| Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:26 +0100 |
bulwahn |
renaming all lemmas with name rel_pow to relpow
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:23 +0100 |
bulwahn |
adding code generation for relpow by copying the ideas for code generation of funpow
|
file |
diff |
annotate
|
| Fri, 27 Jan 2012 17:22:05 +0100 |
bulwahn |
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
|
file |
diff |
annotate
|
| Sun, 01 Jan 2012 11:28:45 +0100 |
haftmann |
cleanup of code declarations
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:12 +0100 |
haftmann |
tuned layout
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 14:48:00 +0200 |
haftmann |
tuned type annnotation
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:35:15 +0200 |
haftmann |
avoid very specific code equation for card; corrected spelling
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:27:46 +0200 |
haftmann |
bouned transitive closure
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:02:59 +0200 |
haftmann |
moved acyclic predicate up in hierarchy
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 22:56:19 +0200 |
haftmann |
modernized definitions
|
file |
diff |
annotate
|
| Mon, 03 Oct 2011 14:43:13 +0200 |
bulwahn |
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|