added examples for Simps_Case_Conv

allowed less exhaustive patterns

use case_of_simps

use case_of_simps

added simps_of_case and case_of_simps to convert between simps and case rules

merged

close window and start process asynchronously;

more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;

recovered cygwin.root from 1c87e79bb838; removed junk;

provide file indicator;

updated windows_app-20130905;

main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator; standardized jdk location;

standardize jdk name; check tar errors;

updated to jdk-7u25; less redundant directory structure;

support only one scala version; tuned;

updated to jedit_build-20130905 which is based on jedit-5.1.0; added jsr305-2.0.0.jar from http://code.google.com/p/findbugs (via ivy cache), which is required to resolve javax.annotation.*;

explicit module names have precedence over identifier declarations

check explicit module names for conformity

list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors

support indirect corecursion

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

tuned proofs;

interpret keys more movement only when needed;

non-persistent print_state: trade-off between JVM space vs. ML time;

some explicit indication of Proof General legacy;

merge

various refactoring; handle self-mappings; handle range types containing function types;

expose basic Symbol.properties (uninterpreted);

tuned proofs;

remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does;

no completion on backspace -- too intrusive, e.g. when deleting keywords;

more contributors;

updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);

updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP;

included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;

updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;

brought up to date with TPTP_Proof;

using richer annotation from formula annotations in proof;

extracting more info from formula annotation in proof;

corrected syntax filter;

reading tptp status code;

improved handling of nonstandard problem names;

merged

merged

tuned proofs -- less guessing;

cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;

minor tuning;

cases: more position information and PIDE markup;

more liberal 'case' syntax: allow parentheses without arguments;

more robust ToyList_Test;

Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);

tuned proofs -- clarified flow of facts wrt. calculation;

proper imports; tuned proofs;

tuned proof;

more explicit indication of 'guess' as improper Isar (aka "script") element;

Further clarifies sublocale and rewrite morphisms.

Clarifies that interpretation does not only apply to facts, but to declaratoins in general.

Clarifies documentation of interpretation in local theories.

New test case: interpretation in named contexts is not persistent.

Terminology: mixin -> rewrite morphism.

merged

added lemmas

merged

NEWS

move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems

handle direct corecursion

updated according to bceec99254b0;

improved interfaces

simplified rewriting of map arguments

remove redundant (simp del: ..)

modernized more examples

merged

modernized example

honor mixfix specifications

merge

simplified recursive calls' replacement

merged

tuned proofs;

tuned proofs;

provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;

uniform abbrevs for left/right arrows;

more abbrevs according to Isabelle/HOL ASCII replacement syntax;

added common alternative for == (its ambiguity also avoids conflict with ==>); clarified (= )= [= ]= (like <= >=); removed * (too intrusive);

more accurate description: Swing/L&F has additional handlers;

handle selector formulae with no corecursive calls

merged

tuned proofs;

simplified (see 7c39677f9ea0);

sort items according to persistent history of frequency of use;

more general backup files;

fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)