2013-09-06 wenzelm 2013-09-06 more standard header;
2013-09-06 wenzelm 2013-09-06 updated keywords;
2013-09-06 noschinl 2013-09-06 merged
2013-09-06 noschinl 2013-09-06 added examples for Simps_Case_Conv
2013-09-06 noschinl 2013-09-06 allowed less exhaustive patterns
2013-09-06 noschinl 2013-09-06 use case_of_simps
2013-09-06 noschinl 2013-09-06 use case_of_simps
2013-09-06 noschinl 2013-09-06 added simps_of_case and case_of_simps to convert between simps and case rules
2013-09-05 wenzelm 2013-09-05 merged
2013-09-05 wenzelm 2013-09-05 close window and start process asynchronously;
2013-09-05 wenzelm 2013-09-05 more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
2013-09-05 wenzelm 2013-09-05 recovered cygwin.root from 1c87e79bb838; removed junk;
2013-09-05 wenzelm 2013-09-05 provide file indicator;
2013-09-05 wenzelm 2013-09-05 updated windows_app-20130905;
2013-09-05 wenzelm 2013-09-05 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator; standardized jdk location;
2013-09-05 wenzelm 2013-09-05 standardize jdk name; check tar errors;
2013-09-05 wenzelm 2013-09-05 updated to jdk-7u25; less redundant directory structure;
2013-09-05 wenzelm 2013-09-05 support only one scala version; tuned;
2013-09-05 wenzelm 2013-09-05 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.*;
2013-09-05 haftmann 2013-09-05 explicit module names have precedence over identifier declarations
2013-09-05 haftmann 2013-09-05 check explicit module names for conformity
2013-09-05 traytel 2013-09-05 list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
2013-09-05 panny 2013-09-05 support indirect corecursion
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 interpret keys more movement only when needed;
2013-09-04 wenzelm 2013-09-04 non-persistent print_state: trade-off between JVM space vs. ML time;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-09-04 panny 2013-09-04 merge
2013-09-04 panny 2013-09-04 various refactoring; handle self-mappings; handle range types containing function types;
2013-09-04 wenzelm 2013-09-04 expose basic Symbol.properties (uninterpreted);
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 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;
2013-09-04 wenzelm 2013-09-04 no completion on backspace -- too intrusive, e.g. when deleting keywords;
2013-09-04 wenzelm 2013-09-04 more contributors;
2013-09-03 sultana 2013-09-03 updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);
2013-09-03 sultana 2013-09-03 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;
2013-09-03 sultana 2013-09-03 included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;
2013-09-03 sultana 2013-09-03 updated syntax to use 'ML_file' rather than 'uses';
2013-09-03 sultana 2013-09-03 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;
2013-09-03 sultana 2013-09-03 get_file_list now returns files sorted by size;
2013-09-03 sultana 2013-09-03 brought up to date with TPTP_Proof;
2013-09-03 sultana 2013-09-03 using richer annotation from formula annotations in proof;
2013-09-03 sultana 2013-09-03 extracting more info from formula annotation in proof;
2013-09-03 sultana 2013-09-03 corrected syntax filter;
2013-09-03 sultana 2013-09-03 reading tptp status code;
2013-09-03 sultana 2013-09-03 improved handling of nonstandard problem names;
2013-09-03 wenzelm 2013-09-03 merged
2013-09-03 wenzelm 2013-09-03 merged
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-09-03 wenzelm 2013-09-03 cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;
2013-09-03 wenzelm 2013-09-03 minor tuning;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-09-03 wenzelm 2013-09-03 more liberal 'case' syntax: allow parentheses without arguments;
2013-09-03 wenzelm 2013-09-03 more robust ToyList_Test;
2013-09-03 wenzelm 2013-09-03 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);
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;