updated to jedit_build-20131106 (Console.jar 5.1.3);

join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;

tuned signature;

less tiny font for search criteria;

tuned tooltips;

swap equations and premises in the coinductive step for better proof automation

no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;

tuned;

CONTRIBUTORS

more on text completion;

tuned;

more on Monitor panel;

more on Timing;

more on miscellaneous tools;

more screenshots;

more screenshots;

more on Sledgehammer; more on Find;

more on automatically tried tools;

more on prover output; more sections;

misc tuning and clarification;

more on file-system access; provide ISABELLE_HOME_USER as well;

tuned;

more on problems and workarounds;

tuned;

clarified isabelle options -l;

tuned;

clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);

removed dead code (see also db4bf4fb5492);

Added tag Isabelle2013-1-RC3 for changeset fbcaa9f08879

avoid non-portable int constant -- make SML/NJ happy;

avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;

prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;

basic IO buffer size like for fifo -- imitate implicit flushing behaviour more closely;

removed junk (cf. 409d7f7247f4);

fix a citation

declare Quotient_Examples/FSet.thy as almost obsolete

update documentation of important public ML functions in Lifting

update documentation of Lifting/Transfer and Quotient

don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.

tuned;

more screenshots; tuned;

tuned;

misc tuning;

more strict find_command -- avoid invalid hyperlink_command;

more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;

obsolete;

clarified Editor.current_command: allow outdated snapshot; more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

make double sure that AWT/Swing antialiasing is enabled (see also http://www.jedit.org/users-guide/jvm-options.html and jdk/src/share/classes/sun/awt/SunToolkit.java);

more documentation;

more documentation;

more documentation;

tuned;

NEWS;

avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);

add congruence rule to prevent code_simp from looping

Added tag Isabelle2013-1-RC2 for changeset 782e430e6a83

native executable for Linux (see Admin/Linux);

proper NULL termination;

native executable even for Linux, to avoid surprises with file managers opening executable script as text file;

proper warning at run time, not in the parser;

prefer "fresh" open -- requires Lion / Mountain Lion;

clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;

prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)

more parallelism in blocking mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

another shortcut alias;

NEWS;

Added tag Isabelle2013-1-RC1 for changeset c37100233af7

reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code

removed dead code

added check to avoid odd situations the N2M code cannot handle

reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)

tuned signature

handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)

tuned

tuned

qualifed popular user space names

dropped obsolete check: dest_num always yields positive number

simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

more exercises

by (auto ...)[1] not by (auto [1])

added exercise

Add output translation for <a := .., b := .., ..> state notation.

reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)

more docs

properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel

reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP

simplified code

fourth attempt at generalizing N2M types (to leverage caching)

tuning

int and nat are conditionally_complete_lattices

be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'

removed dead code

update docs

take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case

took out loopy code

take out even less aggressive generalization -- it's still too aggressive

reverted too aggressive 7cb8442298f0

generalize more aggressively

avoid subtle failure in the presence of top sort

tuning

get mutually recursive maps as well

tuned proofs in Approximation

fixed subtle name shadowing bug

use right permutation in 'map2'

stronger normalization, to increase n2m cache effectiveness

make local theory operations non-pervasive (makes more intuitive sense)

NEWS

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

generalize bdd_above/below_uminus to ordered_ab_group_add

restrict Limsup and Liminf to complete lattices

use INF and SUP on conditionally complete lattices in multivariate analysis

add SUP and INF for conditionally complete lattices

use bdd_above and bdd_below for conditionally complete lattices

generalize SUP and INF to the syntactic type classes Sup and Inf

added some N2M caching

also generalize fixed types

generalize types when synthetizing n2m (co)recursors, to facilitate reuse

nicer error message in case of duplicates

use int example like in the rest of IMP (instead of nat)