ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51515
Fix issue related to mixins in roundup.
Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.
kleing [Mon, 25 Mar 2013 15:18:44 +0100] rev 51514
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
nipkow [Mon, 25 Mar 2013 15:09:41 +0100] rev 51513
added lemmas
wenzelm [Mon, 25 Mar 2013 14:07:59 +0100] rev 51512
merged
wenzelm [Mon, 25 Mar 2013 14:04:01 +0100] rev 51511
clarified text_fold vs. fbrk;
wenzelm [Mon, 25 Mar 2013 13:37:44 +0100] rev 51510
tuned print_classes: more standard order, markup, formatting;
uniform printing of minimal supersort/classrel;
wenzelm [Mon, 25 Mar 2013 11:05:07 +0100] rev 51509
tuned message;
wenzelm [Mon, 25 Mar 2013 10:45:47 +0100] rev 51508
actually exit on scalac failure;
wenzelm [Mon, 25 Mar 2013 10:37:38 +0100] rev 51507
tuned signature;
kleing [Mon, 25 Mar 2013 13:50:50 +0100] rev 51506
removed obsolete uses of ext
wenzelm [Sun, 24 Mar 2013 16:19:54 +0100] rev 51505
prefer preset = 3 -- much faster and less memory requirement;
wenzelm [Sun, 24 Mar 2013 16:12:45 +0100] rev 51504
basic support for xz files;
wenzelm [Sun, 24 Mar 2013 16:10:19 +0100] rev 51503
added component xz-java-1.2;
wenzelm [Sun, 24 Mar 2013 14:26:10 +0100] rev 51502
more "quick start" hints;
more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle";
tuned;
traytel [Sun, 24 Mar 2013 12:07:31 +0100] rev 51501
simple case syntax for stream (stolen from AFP/Coinductive)
wenzelm [Sat, 23 Mar 2013 21:48:03 +0100] rev 51500
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
tuned proofs;
wenzelm [Sat, 23 Mar 2013 21:19:10 +0100] rev 51499
merged
wenzelm [Sat, 23 Mar 2013 21:13:03 +0100] rev 51498
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
wenzelm [Sat, 23 Mar 2013 19:54:15 +0100] rev 51497
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
wenzelm [Sat, 23 Mar 2013 19:39:31 +0100] rev 51496
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm [Sat, 23 Mar 2013 16:46:09 +0100] rev 51495
apply small result immediately, to avoid visible delay of text update after window move;
wenzelm [Sat, 23 Mar 2013 16:10:46 +0100] rev 51494
structural equality for Command.Results;
more general Command.State.eq_content;
wenzelm [Sat, 23 Mar 2013 13:57:46 +0100] rev 51493
allow fractional pretty margin -- avoid premature rounding;
wenzelm [Sat, 23 Mar 2013 13:12:39 +0100] rev 51492
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
wenzelm [Sat, 23 Mar 2013 13:04:28 +0100] rev 51491
tuned;
haftmann [Sat, 23 Mar 2013 20:57:57 +0100] rev 51490
spelling
haftmann [Sat, 23 Mar 2013 20:50:39 +0100] rev 51489
fundamental revision of big operators on sets
haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51488
tuned proof
haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51487
locales for abstract orders
krauss [Sat, 23 Mar 2013 07:30:53 +0100] rev 51486
merged
krauss [Fri, 22 Mar 2013 00:39:16 +0100] rev 51485
added rudimentary induction rule for partial_function (heap)
krauss [Fri, 22 Mar 2013 00:39:14 +0100] rev 51484
allow induction predicates with arbitrary arity (not just binary)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51483
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51482
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51481
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51480
move connected to HOL image; used to show intermediate value theorem
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51479
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51478
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51477
clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51476
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51475
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51474
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51473
move first_countable_topology to the HOL image
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51472
move metric_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:42 +0100] rev 51471
move topological_space to its own theory
wenzelm [Thu, 21 Mar 2013 16:58:14 +0100] rev 51470
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm [Thu, 21 Mar 2013 16:35:53 +0100] rev 51469
eliminated char_width_int to avoid unclear rounding;
clarified integer conversion for margin;
nipkow [Thu, 21 Mar 2013 10:05:03 +0100] rev 51468
proofs depend only on constraints, not on def of L WHILE
blanchet [Wed, 20 Mar 2013 15:35:35 +0100] rev 51467
use the right role for SPASS hypotheses
kleing [Wed, 20 Mar 2013 14:56:30 +0100] rev 51466
soundness statement as in type system
kleing [Wed, 20 Mar 2013 11:32:16 +0100] rev 51465
add label for referencing in semantics book
nipkow [Wed, 20 Mar 2013 11:16:31 +0100] rev 51464
tuned
nipkow [Tue, 19 Mar 2013 21:35:15 +0100] rev 51463
get rid of xcolor warnings
traytel [Tue, 19 Mar 2013 15:59:58 +0100] rev 51462
extended stream library
kleing [Tue, 19 Mar 2013 14:04:53 +0100] rev 51461
export datatype definition which gets expanded too much in antiquotation
nipkow [Tue, 19 Mar 2013 14:07:13 +0100] rev 51460
tuned
Andreas Lochbihler [Tue, 19 Mar 2013 13:19:21 +0100] rev 51459
add induction rule for partial_function (tailrec)
wenzelm [Mon, 18 Mar 2013 20:02:37 +0100] rev 51458
prefer ownerless window, to avoid question of potentially changing parent view;
wenzelm [Mon, 18 Mar 2013 19:33:25 +0100] rev 51457
proper parent component for window.init;
kleing [Mon, 18 Mar 2013 19:20:53 +0100] rev 51456
lemma names and a corollary
kleing [Mon, 18 Mar 2013 14:47:20 +0100] rev 51455
managed to eliminate further snippets
kleing [Mon, 18 Mar 2013 14:27:38 +0100] rev 51454
fewer IMP snippets
wenzelm [Mon, 18 Mar 2013 13:18:42 +0100] rev 51453
merged
wenzelm [Mon, 18 Mar 2013 11:29:50 +0100] rev 51452
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm [Mon, 18 Mar 2013 11:04:59 +0100] rev 51451
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
wenzelm [Sun, 17 Mar 2013 22:02:06 +0100] rev 51450
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
wenzelm [Sun, 17 Mar 2013 21:04:38 +0100] rev 51449
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
nipkow [Mon, 18 Mar 2013 12:31:13 +0100] rev 51448
tuned
traytel [Mon, 18 Mar 2013 11:25:24 +0100] rev 51447
eliminate duplicated constant (diag vs. Id_on)
traytel [Mon, 18 Mar 2013 11:05:33 +0100] rev 51446
hide internal constants; tuned proofs
nipkow [Mon, 18 Mar 2013 10:28:42 +0100] rev 51445
tuned
nipkow [Sun, 17 Mar 2013 20:29:26 +0100] rev 51444
tuned
nipkow [Sun, 17 Mar 2013 20:27:13 +0100] rev 51443
added advanced rule induction subsection
wenzelm [Sat, 16 Mar 2013 21:44:04 +0100] rev 51442
merged
wenzelm [Sat, 16 Mar 2013 21:26:44 +0100] rev 51441
more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm [Sat, 16 Mar 2013 17:16:39 +0100] rev 51440
some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
wenzelm [Sat, 16 Mar 2013 12:46:22 +0100] rev 51439
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors);
early initialization of gutter to get proper text area painter size (see also 2585c81d840a);
kuncar [Sat, 16 Mar 2013 20:51:47 +0100] rev 51438
drop a workaround because of 8739f8abbecb
kuncar [Sat, 16 Mar 2013 20:51:23 +0100] rev 51437
fixing transfer tactic - unfold fully identity relation by using relator_eq
nipkow [Sat, 16 Mar 2013 17:22:05 +0100] rev 51436
tuned (in particular bold fonts)
wenzelm [Sat, 16 Mar 2013 10:50:23 +0100] rev 51435
merged
wenzelm [Thu, 14 Mar 2013 16:49:36 +0100] rev 51434
document ISABELLE_POLYML;
nipkow [Fri, 15 Mar 2013 18:49:40 +0100] rev 51433
tuned
wenzelm [Fri, 15 Mar 2013 13:46:37 +0100] rev 51432
simplified time_CPU and time_GC;
derive relative speed from time (considered as step function);
wenzelm [Fri, 15 Mar 2013 10:49:28 +0100] rev 51431
updated to scala-2.10.1;
traytel [Fri, 15 Mar 2013 10:08:23 +0100] rev 51430
extended stream library (sdrop_while)
wenzelm [Thu, 14 Mar 2013 14:25:55 +0100] rev 51429
tuned signature;
wenzelm [Thu, 14 Mar 2013 14:14:58 +0100] rev 51428
more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;
wenzelm [Thu, 14 Mar 2013 13:57:44 +0100] rev 51427
proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm [Thu, 14 Mar 2013 13:52:22 +0100] rev 51426
made SML/NJ happy;
nipkow [Thu, 14 Mar 2013 10:51:28 +0100] rev 51425
tuned
wenzelm [Wed, 13 Mar 2013 22:46:28 +0100] rev 51424
merged
wenzelm [Wed, 13 Mar 2013 21:25:08 +0100] rev 51423
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;
wenzelm [Wed, 13 Mar 2013 17:15:25 +0100] rev 51422
proper formatting, to facilitate line-based diff;
wenzelm [Wed, 13 Mar 2013 17:13:22 +0100] rev 51421
more uniform session descriptions, which show up in chapter index;
wenzelm [Wed, 13 Mar 2013 17:06:45 +0100] rev 51420
proper index for HOL-Proofs, which is also in chapter "HOL";
wenzelm [Wed, 13 Mar 2013 16:57:05 +0100] rev 51419
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
wenzelm [Wed, 13 Mar 2013 16:04:16 +0100] rev 51418
more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
wenzelm [Wed, 13 Mar 2013 15:12:14 +0100] rev 51417
sessions may be organized via 'chapter' in ROOT;
wenzelm [Wed, 13 Mar 2013 15:08:38 +0100] rev 51416
do not absorb I/O errors;
wenzelm [Wed, 13 Mar 2013 14:57:16 +0100] rev 51415
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
paulson [Wed, 13 Mar 2013 17:17:33 +0000] rev 51414
new lemma subset_decode_imp_le
kleing [Wed, 13 Mar 2013 16:03:55 +0100] rev 51413
merged
kleing [Wed, 13 Mar 2013 16:03:40 +0100] rev 51412
more IMP snippets
kuncar [Wed, 13 Mar 2013 14:33:15 +0100] rev 51411
rename fset_member to fmember and prove parametricity
traytel [Wed, 13 Mar 2013 13:23:16 +0100] rev 51410
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel [Wed, 13 Mar 2013 10:47:00 +0100] rev 51409
nitpick setup and code generation for streams
nipkow [Wed, 13 Mar 2013 10:15:01 +0100] rev 51408
merged
nipkow [Wed, 13 Mar 2013 10:14:50 +0100] rev 51407
tuned
wenzelm [Tue, 12 Mar 2013 22:44:03 +0100] rev 51406
proper path -- I/O was hidden due to permissiveness;
wenzelm [Tue, 12 Mar 2013 22:24:01 +0100] rev 51405
merged
wenzelm [Tue, 12 Mar 2013 22:22:05 +0100] rev 51404
removed odd cvs artifacts;
wenzelm [Tue, 12 Mar 2013 21:59:48 +0100] rev 51403
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm [Tue, 12 Mar 2013 20:03:04 +0100] rev 51402
include session description in chapter index;
prefer alphabetical order;
wenzelm [Tue, 12 Mar 2013 18:44:48 +0100] rev 51401
tuned;
wenzelm [Tue, 12 Mar 2013 18:30:28 +0100] rev 51400
more accurate theory links;
wenzelm [Tue, 12 Mar 2013 16:47:24 +0100] rev 51399
discontinued "isabelle usedir" option -r (reset session path);
simplified internal session identification: chapter / name;
clarified chapter index (of sessions) vs. session index (of theories);
discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser);
removed obsolete session parent_path;
wenzelm [Mon, 11 Mar 2013 14:25:14 +0100] rev 51398
discontinued "isabelle usedir" option -P (remote path);
wenzelm [Mon, 11 Mar 2013 13:28:46 +0100] rev 51397
support for 'chapter' specifications within session ROOT;
nipkow [Tue, 12 Mar 2013 19:55:17 +0100] rev 51396
added latex markup