Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
use polyml-5.5.1 (SVN), to increase chances of stability of this test;
2013-09-09, by wenzelm
override potential changes in $ISABELLE_HOME_USER/etc/settings;
2013-09-09, by wenzelm
generate application ini based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
2013-09-09, by wenzelm
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
2013-09-09, by wenzelm
tuning
2013-09-09, by blanchet
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
2013-09-09, by blanchet
limit the number of instances of a single theorem
2013-09-09, by blanchet
move metis to new monomorphizer
2013-09-09, by blanchet
use new monomorphizer in Sledgehammer
2013-09-09, by blanchet
tuning
2013-09-09, by blanchet
include map theorems in datastructure for "primcorec"
2013-09-09, by blanchet
enriched data structure with necessary theorems
2013-09-09, by blanchet
updated exe -- more explicit icon;
2013-09-08, by wenzelm
more official lib/logo/isabelle.bmp;
2013-09-08, by wenzelm
use windows_app based on WinRun4J;
2013-09-08, by wenzelm
updated to WinRun4J;
2013-09-08, by wenzelm
tuned whitespace
2013-09-08, by traytel
don't register "sequential" as a keyword for now as this breaks the parser for function
2013-09-08, by traytel
tuned proofs;
2013-09-07, by wenzelm
merged
2013-09-07, by wenzelm
tuned message;
2013-09-07, by wenzelm
tuned message;
2013-09-07, by wenzelm
imitate "isabelle java" and "isabelle jedit" wrt. classpath and options (see also a221a4fdb5a0);
2013-09-07, by wenzelm
generate application wrapper for Linux;
2013-09-07, by wenzelm
observe "stopped" after Cygwin init (which is itself uninterruptible);
2013-09-07, by wenzelm
clarified modules;
2013-09-07, by wenzelm
tuned signature;
2013-09-07, by wenzelm
Cygwin_Init based on System_Dialog;
2013-09-07, by wenzelm
tuned imports;
2013-09-07, by wenzelm
more robust exit;
2013-09-07, by wenzelm
Build_Dialog based on System_Dialog;
2013-09-07, by wenzelm
clarified close operations;
2013-09-07, by wenzelm
clarified result;
2013-09-07, by wenzelm
dialog for system processes, with optional output window;
2013-09-07, by wenzelm
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
2013-09-07, by wenzelm
odd workaround for scalac to enable nohup;
2013-09-07, by wenzelm
odd workaround for scalac to enable nohup;
2013-09-07, by wenzelm
build session before start of jedit;
2013-09-07, by wenzelm
imitate "isabelle java" and "isabelle jedit" wrt. classpath and options;
2013-09-06, by wenzelm
more Proof General legacy;
2013-09-06, by wenzelm
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
2013-09-06, by wenzelm
warm start of Isabelle/jEdit from Isabelle/Scala;
2013-09-06, by wenzelm
prefer explicit thread;
2013-09-06, by wenzelm
tuned proofs;
2013-09-06, by wenzelm
tuned proofs;
2013-09-06, by wenzelm
prefer Isabelle/Scala over bash;
2013-09-06, by wenzelm
prefer Isabelle/Scala over bash;
2013-09-06, by wenzelm
prefer warm start via JEdit_Main;
2013-09-06, by wenzelm
slight cleanup of lemma locations; tuned proof
2013-09-06, by haftmann
tuned
2013-09-06, by haftmann
tuned;
2013-09-06, by wenzelm
tuned;
2013-09-06, by wenzelm
removed junk;
2013-09-06, by wenzelm
more standard header;
2013-09-06, by wenzelm
updated keywords;
2013-09-06, by wenzelm
merged
2013-09-06, by noschinl
added examples for Simps_Case_Conv
2013-09-06, by noschinl
allowed less exhaustive patterns
2013-09-06, by noschinl
use case_of_simps
2013-09-06, by noschinl
use case_of_simps
2013-09-06, by noschinl
added simps_of_case and case_of_simps to convert between simps and case rules
2013-09-06, by noschinl
merged
2013-09-05, by wenzelm
close window and start process asynchronously;
2013-09-05, by wenzelm
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
2013-09-05, by wenzelm
recovered cygwin.root from 1c87e79bb838;
2013-09-05, by wenzelm
provide file indicator;
2013-09-05, by wenzelm
updated windows_app-20130905;
2013-09-05, by wenzelm
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
2013-09-05, by wenzelm
standardize jdk name;
2013-09-05, by wenzelm
updated to jdk-7u25;
2013-09-05, by wenzelm
support only one scala version;
2013-09-05, by wenzelm
updated to jedit_build-20130905 which is based on jedit-5.1.0;
2013-09-05, by wenzelm
explicit module names have precedence over identifier declarations
2013-09-05, by haftmann
check explicit module names for conformity
2013-09-05, by haftmann
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
2013-09-05, by traytel
support indirect corecursion
2013-09-05, by panny
tuned proofs;
2013-09-04, by wenzelm
tuned proofs;
2013-09-04, by wenzelm
tuned proofs;
2013-09-04, by wenzelm
tuned;
2013-09-04, by wenzelm
tuned proofs;
2013-09-04, by wenzelm
interpret keys more movement only when needed;
2013-09-04, by wenzelm
non-persistent print_state: trade-off between JVM space vs. ML time;
2013-09-04, by wenzelm
some explicit indication of Proof General legacy;
2013-09-04, by wenzelm
merge
2013-09-04, by panny
various refactoring;
2013-09-04, by panny
expose basic Symbol.properties (uninterpreted);
2013-09-04, by wenzelm
tuned proofs;
2013-09-04, by wenzelm
remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
2013-09-04, by wenzelm
no completion on backspace -- too intrusive, e.g. when deleting keywords;
2013-09-04, by wenzelm
more contributors;
2013-09-04, by wenzelm
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, by sultana
updated TPTP parser to conform to version 5.4.0;
2013-09-03, by sultana
included axiom formulas (removing a FIXME) in the imported problem;
2013-09-03, by sultana
updated syntax to use 'ML_file' rather than 'uses';
2013-09-03, by sultana
now allowing numeric identifiers to be used in 'file' annotations;
2013-09-03, by sultana
get_file_list now returns files sorted by size;
2013-09-03, by sultana
brought up to date with TPTP_Proof;
2013-09-03, by sultana
using richer annotation from formula annotations in proof;
2013-09-03, by sultana
extracting more info from formula annotation in proof;
2013-09-03, by sultana
corrected syntax filter;
2013-09-03, by sultana
reading tptp status code;
2013-09-03, by sultana
improved handling of nonstandard problem names;
2013-09-03, by sultana
merged
2013-09-03, by wenzelm
merged
2013-09-03, by wenzelm
tuned proofs -- less guessing;
2013-09-03, by wenzelm
cases: formal binding of 'assumes', with position provided via invoke_case;
2013-09-03, by wenzelm
minor tuning;
2013-09-03, by wenzelm
cases: more position information and PIDE markup;
2013-09-03, by wenzelm
more liberal 'case' syntax: allow parentheses without arguments;
2013-09-03, by wenzelm
more robust ToyList_Test;
2013-09-03, by wenzelm
Execution.fork formally requires registered Execution.running;
2013-09-03, by wenzelm
tuned proofs -- clarified flow of facts wrt. calculation;
2013-09-03, by wenzelm
proper imports;
2013-09-03, by wenzelm
tuned proof;
2013-09-02, by wenzelm
more explicit indication of 'guess' as improper Isar (aka "script") element;
2013-09-02, by wenzelm
Further clarifies sublocale and rewrite morphisms.
2013-09-03, by ballarin
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
2013-09-03, by ballarin
Clarifies documentation of interpretation in local theories.
2013-09-03, by ballarin
New test case: interpretation in named contexts is not persistent.
2013-09-03, by ballarin
Terminology: mixin -> rewrite morphism.
2013-09-03, by ballarin
merged
2013-09-02, by nipkow
added lemmas
2013-09-02, by nipkow
merged
2013-09-02, by Andreas Lochbihler
NEWS
2013-09-02, by Andreas Lochbihler
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
2013-09-02, by Andreas Lochbihler
handle direct corecursion
2013-09-02, by panny
updated according to bceec99254b0;
2013-09-02, by wenzelm
improved interfaces
2013-09-01, by panny
simplified rewriting of map arguments
2013-09-01, by panny
remove redundant (simp del: ..)
2013-09-01, by kleing
modernized more examples
2013-09-01, by traytel
merged
2013-08-31, by traytel
modernized example
2013-08-31, by traytel
honor mixfix specifications
2013-08-31, by traytel
merge
2013-08-31, by panny
simplified recursive calls' replacement
2013-08-31, by panny
merged
2013-08-31, by wenzelm
tuned proofs;
2013-08-31, by wenzelm
tuned proofs;
2013-08-31, by wenzelm
provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;
2013-08-31, by wenzelm
uniform abbrevs for left/right arrows;
2013-08-31, by wenzelm
more abbrevs according to Isabelle/HOL ASCII replacement syntax;
2013-08-31, by wenzelm
added common alternative for == (its ambiguity also avoids conflict with ==>);
2013-08-31, by wenzelm
more accurate description: Swing/L&F has additional handlers;
2013-08-31, by wenzelm
handle selector formulae with no corecursive calls
2013-08-31, by panny
merged
2013-08-31, by wenzelm
tuned proofs;
2013-08-31, by wenzelm
simplified (see 7c39677f9ea0);
2013-08-30, by wenzelm
sort items according to persistent history of frequency of use;
2013-08-30, by wenzelm
more general backup files;
2013-08-30, by wenzelm
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
2013-08-30, by panny
some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;
2013-08-30, by wenzelm
tuned proofs;
2013-08-30, by wenzelm
Doc improvements
2013-08-30, by traytel
prove theorem in the right context (that knows about local variables)
2013-08-30, by traytel
fixed docs w.r.t. availability of "primrec_new" and friends
2013-08-30, by blanchet
more canonical naming
2013-08-30, by blanchet
more set syntax
2013-08-30, by nipkow
merged
2013-08-30, by wenzelm
NEWS;
2013-08-30, by wenzelm
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
2013-08-30, by wenzelm
explicit is always immediate;
2013-08-30, by wenzelm
single-letter abbrev does not make sense -- too many candidates;
2013-08-30, by wenzelm
allow short words for explicit completion;
2013-08-30, by wenzelm
fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;
2013-08-30, by wenzelm
more symbol abbrevs;
2013-08-30, by wenzelm
misc tuning -- reduce conflicts;
2013-08-30, by wenzelm
allow multiple entries;
2013-08-30, by wenzelm
more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
2013-08-30, by wenzelm
allow multiple symbol properties, notably groups and abbrevs;
2013-08-30, by wenzelm
private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;
2013-08-30, by wenzelm
check tar error, e.g. from corrupted download;
2013-08-30, by wenzelm
less surprising immediate completion;
2013-08-30, by wenzelm
updated keywords
2013-08-30, by blanchet
tuned theory name
2013-08-30, by blanchet
moved keywords down the hierarchy
2013-08-30, by blanchet
renamed command to clarify connection with BNF
2013-08-30, by blanchet
merged two theory files
2013-08-30, by blanchet
updated news/contributors with BNF stuff
2013-08-30, by blanchet
added example
2013-08-30, by blanchet
rationalized files
2013-08-30, by blanchet
polished newly included files after moving
2013-08-30, by blanchet
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
2013-08-30, by blanchet
tuned proofs;
2013-08-30, by wenzelm
merged
2013-08-29, by traytel
qualify internal and external constants in {l,g}fp properly
2013-08-29, by traytel
merged
2013-08-29, by wenzelm
merged
2013-08-29, by wenzelm
border as for Pretty_Tooltip;
2013-08-29, by wenzelm
less aggressive immediate completion, based on input and text;
2013-08-29, by wenzelm
preserve original word -- relevant for true uniqueness of immediate completion;
2013-08-29, by wenzelm
tuned;
2013-08-29, by wenzelm
added action isabelle.complete, using standard jEdit keyboard shortcut;
2013-08-29, by wenzelm
option to insert unique completion immediately into buffer;
2013-08-29, by wenzelm
tuned proofs;
2013-08-29, by wenzelm
renamed BNF fact
2013-08-29, by blanchet
renamed BNF axiom
2013-08-29, by blanchet
renamed BNF fact
2013-08-29, by blanchet
renamed BNF axiom
2013-08-29, by blanchet
compile
2013-08-29, by blanchet
renamed BNF fact
2013-08-29, by blanchet
make SML/NJ happy
2013-08-29, by kuncar
merged
2013-08-29, by wenzelm
tuned proofs;
2013-08-29, by wenzelm
clarified SideKick parser name, which serves as quasi "mode" here;
2013-08-29, by wenzelm
explicit indication of outer syntax with no tokens;
2013-08-29, by wenzelm
clarified module location;
2013-08-29, by wenzelm
always use extended styles (despite de26cf3191a3);
2013-08-29, by wenzelm
more uniform configuration of editor modes and token markers;
2013-08-29, by wenzelm
syntax for isabelle-news with symbol completion;
2013-08-29, by wenzelm
tuned signature;
2013-08-29, by wenzelm
maintain Completion_Popup.Text_Area as client property like Document_View;
2013-08-29, by wenzelm
some completion options;
2013-08-29, by wenzelm
more abstract Completion_Popup.Text_Area;
2013-08-29, by wenzelm
GTK+ works better due to avoidance of default list view popups;
2013-08-29, by wenzelm
renamed BNF axiom
2013-08-29, by blanchet
merge
2013-08-29, by blanchet
handle type class annotations on (co)datatype parameters gracefully
2013-08-29, by blanchet
store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
2013-08-29, by traytel
cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
2013-08-29, by blanchet
qualify BNF constants properly
2013-08-29, by blanchet
qualify generated constants uniformly
2013-08-29, by blanchet
rationalized bindings
2013-08-29, by blanchet
rationalize message generation + added a warning
2013-08-29, by blanchet
removed outdated comments
2013-08-29, by panny
build relator term for compound type (generalized build_map)
2013-08-29, by traytel
documentation ideas
2013-08-29, by blanchet
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
2013-08-29, by blanchet
merge
2013-08-29, by blanchet
more
2013-08-29, by blanchet
tuned proofs;
2013-08-29, by wenzelm
merged
2013-08-28, by wenzelm
tuned proofs;
2013-08-28, by wenzelm
tuned proofs;
2013-08-28, by wenzelm
complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text;
2013-08-28, by wenzelm
tuned signature -- no need for ooddities;
2013-08-28, by wenzelm
tuned -- help finding rare NPE on cold start;
2013-08-28, by wenzelm
tuned proofs;
2013-08-28, by wenzelm
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-28, by wenzelm
more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
2013-08-28, by wenzelm
tuned;
2013-08-28, by wenzelm
dismiss popups more uniformly;
2013-08-28, by wenzelm
more uniform check (see JEdit_Lib.propagate_key);
2013-08-28, by wenzelm
tuned signature;
2013-08-28, by wenzelm
more symbols;
2013-08-28, by wenzelm
tuned proofs;
2013-08-27, by wenzelm
tuned proofs;
2013-08-27, by wenzelm
tuned proofs;
2013-08-27, by wenzelm
enable jEdit KeyEventWorkaround uniformly;
2013-08-27, by wenzelm
de-register completion first, which is important to make new popup reliably;
2013-08-27, by wenzelm
register single instance within root, in order to get rid of old popup as user continues typing;
2013-08-27, by wenzelm
more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
2013-08-27, by wenzelm
some actual completion via outer syntax;
2013-08-27, by wenzelm
tuned signature;
2013-08-27, by wenzelm
avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
2013-08-27, by wenzelm
determine completion geometry like tooltip;
2013-08-27, by wenzelm
explicit "hidden" operation with focus management;
2013-08-27, by wenzelm
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
2013-08-27, by wenzelm
more standard key handling according to jEdit (with workaround);
2013-08-27, by wenzelm
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-27, by wenzelm
got rid of old error -- users who install SPASS manually are responsible for any version mismatches
2013-08-28, by blanchet
tuned messages
2013-08-28, by blanchet
natural component order
2013-08-28, by blanchet
better error message
2013-08-28, by blanchet
tuning
2013-08-28, by blanchet
tuned
2013-08-28, by nipkow
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
2013-08-28, by kuncar
merged
2013-08-28, by nipkow
added rtrancl_while
2013-08-28, by nipkow
renamed inner_dense_linorder to dense_linorder
2013-08-27, by hoelzl
renamed typeclass dense_linorder to unbounded_dense_linorder
2013-08-27, by hoelzl
tuned imports;
2013-08-26, by wenzelm
another sample found by Stefan Berghofer;
2013-08-26, by wenzelm
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
2013-08-26, by wenzelm
allow NUL characters in ML string passed to C library;
2013-08-26, by wenzelm
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
2013-08-26, by blanchet
merged
2013-08-26, by wenzelm
prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
2013-08-26, by wenzelm
prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;
2013-08-26, by wenzelm
always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);
2013-08-26, by wenzelm
proper context;
2013-08-26, by wenzelm
tuned
2013-08-26, by traytel
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
2013-08-26, by traytel
export one more ML function, needed for primcorec
2013-08-26, by blanchet
reverted 6c5e7143e1f6; took a better look at evaluation data this time
2013-08-26, by blanchet
tuned unchecked ML;
2013-08-26, by wenzelm
removed junk;
2013-08-26, by wenzelm
ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;
2013-08-26, by wenzelm
tuned fudge factor in light of evaluation
2013-08-26, by blanchet
tuned proofs;
2013-08-25, by wenzelm
tuned proofs;
2013-08-25, by wenzelm
discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;
2013-08-25, by wenzelm
tuned;
2013-08-25, by wenzelm
maintain goal forks as part of global execution;
2013-08-25, by wenzelm
tuned proofs -- fewer warnings;
2013-08-25, by wenzelm
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
2013-08-25, by wenzelm
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
2013-08-25, by wenzelm
some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
2013-08-25, by wenzelm
use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);
2013-08-25, by wenzelm
tuned proofs;
2013-08-24, by wenzelm
tuned proofs;
2013-08-24, by wenzelm
confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
2013-08-24, by wenzelm
strict checking of coordinates wrt. inner painter component;
2013-08-24, by wenzelm
more static values;
2013-08-24, by wenzelm
support more brackets;
2013-08-24, by wenzelm
prefer static "control", which is determined when the mouse event happens, not when its action runs;
2013-08-24, by wenzelm
tuned signature;
2013-08-24, by wenzelm
more precise painting;
2013-08-24, by wenzelm
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
2013-08-24, by wenzelm
clarified border (again, see also 7ce3ebc268a1);
2013-08-24, by wenzelm
more faithful representation of U+2983 and U+2984 as "white" curly braces -- based on braces and bar from cmsy10.pfb;
2013-08-24, by wenzelm
prefer plain subscript for notation;
2013-08-23, by wenzelm
merged
2013-08-23, by wenzelm
more standard parser combinator expressions and tool setup;
2013-08-23, by wenzelm
added Theory.setup convenience;
2013-08-23, by wenzelm
more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);
2013-08-23, by wenzelm
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
2013-08-23, by wenzelm
tuned signature;
2013-08-23, by wenzelm
discontinued unused antiquotation blocks;
2013-08-23, by wenzelm
missing ROOT (cf. beb4ee344c22);
2013-08-23, by wenzelm
more modular setup;
2013-08-23, by wenzelm
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
2013-08-23, by wenzelm
removed unused ML antiquotations @{let}, @{note};
2013-08-23, by wenzelm
obsolete (see 52790e3961fe);
2013-08-23, by wenzelm
added action isabelle.reset-font-size;
2013-08-23, by wenzelm
tuned -- some reformatting;
2013-08-23, by wenzelm
repaired num_extra_feature_facts + tuning
2013-08-23, by blanchet
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
2013-08-23, by blanchet
removed obsolete file
2013-08-23, by blanchet
minor MaSh fix
2013-08-23, by blanchet
eliminated some needless MaSh features
2013-08-23, by blanchet
tuned output
2013-08-23, by blanchet
better tracing + honor blocking better
2013-08-23, by blanchet
learn new facts on query if there aren't too many of them in MaSh
2013-08-23, by blanchet
remove OP
2013-08-23, by kuncar
increase relevance of unknown proximate facts
2013-08-22, by blanchet
fixed pattern matching
2013-08-22, by blanchet
fixed subtle bug with "take" + thread overlord through
2013-08-22, by blanchet
separate tracing option for code_simp
2013-08-22, by haftmann
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
2013-08-22, by haftmann
delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned
2013-08-22, by kuncar
publish a private function
2013-08-22, by kuncar
configuration option to control timing output for (co)datatypes
2013-08-22, by traytel
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
2013-08-22, by blanchet
take chained and proximate facts into consideration when computing MaSh features
2013-08-22, by blanchet
pour extra features from proximate facts into goal, in exporter
2013-08-22, by blanchet
cleanup old duplicated functionality
2013-08-22, by blanchet
store theorem about composition of fold and map in fp_result
2013-08-22, by traytel
tuning
2013-08-22, by blanchet
ideas for (co)datatype docs
2013-08-22, by blanchet
minor tweaks to MaSh tool
2013-08-22, by blanchet
added datatype example
2013-08-22, by blanchet
support more brackets;
2013-08-21, by wenzelm
prefer text version of single angle quotation marks: U+2039 and U+203A from DejaVuSansMono;
2013-08-21, by wenzelm
double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
2013-08-21, by kuncar
improve weight computation for complex terms
2013-08-21, by blanchet
improved support for MaSh server
2013-08-21, by blanchet
get rid of some silly MaSh features
2013-08-21, by blanchet
weight MaSh constants by frequency
2013-08-21, by blanchet
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)
2013-08-21, by traytel
reference to datatype refinment paper
2013-08-21, by haftmann
tuned theory imports
2013-08-21, by traytel
avoid constructor name clash
2013-08-21, by blanchet
renamed theory files to be closer to (new) command names
2013-08-21, by blanchet
only generate feature weights for queries -- they're not used elsewhere
2013-08-21, by blanchet
generate max suggestions in MaSh export driver
2013-08-21, by blanchet
new version of MaSh tool, with more server bugfixes
2013-08-21, by blanchet
take out dangerous feature, now that all updates are permanent
2013-08-21, by blanchet
use new MaSh command-line arguments
2013-08-21, by blanchet
shutdown MaSh server
2013-08-21, by blanchet
new version of MaSh tool, with less broken server
2013-08-21, by blanchet
merged
2013-08-20, by wenzelm
more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;
2013-08-20, by wenzelm
proper exhaustive match (cf. e9beabf045ab);
2013-08-20, by wenzelm
proper context;
2013-08-20, by wenzelm
merged
2013-08-20, by krauss
renamed theory Mrec to Legacy_Mrec, no longer included by default
2013-08-20, by krauss
replaced use of obsolete MREC by partial_function (heap)
2013-08-20, by krauss
more document antiquotations (for proper theorem names);
2013-08-17, by Christian Sternagel
moved derivation of strong coinduction to sugar
2013-08-20, by traytel
simpler (forward) derivation of strong (up-to equality) coinduction properties
2013-08-20, by traytel
don't derive unused low-level theorem
2013-08-20, by traytel
tuned example
2013-08-20, by traytel
doc tuning
2013-08-20, by blanchet
adapted ML code to new version of MaSh tool
2013-08-20, by blanchet
new version of MaSh tool -- experimental server
2013-08-20, by blanchet
adapted to new MaSh syntax
2013-08-20, by blanchet
tuning
2013-08-20, by blanchet
merged
2013-08-20, by paulson
Inserted footnote under match_tac
2013-08-20, by paulson
learn MaSh facts on the fly
2013-08-20, by blanchet
allow MaSh query to do some learning as well
2013-08-20, by blanchet
tuning
2013-08-20, by blanchet
merged
2013-08-20, by blanchet
removed french option to manuals
2013-08-20, by blanchet
treat frees as both consts and vars, for more hits
2013-08-19, by blanchet
keep long names to stay on the safe side
2013-08-19, by blanchet
tuned;
2013-08-19, by wenzelm
tuned signature;
2013-08-19, by wenzelm
MaSh tweaking: shorter names + killed (broken) SNoW
2013-08-19, by blanchet
handle Bounds as well in MaSh features
2013-08-19, by blanchet
add subtypes as well as features in MaSh
2013-08-19, by blanchet
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
2013-08-19, by blanchet
generate deep type patterns in MaSh
2013-08-19, by blanchet
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
2013-08-19, by blanchet
tuned;
2013-08-18, by wenzelm
tuned proofs;
2013-08-18, by wenzelm
more static simpsets, which also avoids spurious warnings due to duplicate rules provided here;
2013-08-18, by wenzelm
more symbols;
2013-08-18, by wenzelm
more symbols;
2013-08-18, by wenzelm
merged
2013-08-18, by wenzelm
load_theories if continuous_checking;
2013-08-18, by wenzelm
discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
2013-08-18, by wenzelm
prefer plain subscript;
2013-08-18, by wenzelm
tuned;
2013-08-18, by wenzelm
spelling and typos
2013-08-18, by haftmann
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
2013-08-18, by haftmann
relaxed preconditions
2013-08-18, by haftmann
type class for generic division algorithm on numerals
2013-08-18, by haftmann
added lemma
2013-08-18, by haftmann
added lemma
2013-08-18, by haftmann
generalized sort constraint of lemmas
2013-08-18, by haftmann
explicit conversion from and to bool, and into algebraic structures with 0 and 1
2013-08-18, by haftmann
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
2013-08-18, by haftmann
more markup;
2013-08-18, by wenzelm
tuned;
2013-08-18, by wenzelm
updated identifier syntax;
2013-08-18, by wenzelm
Sledgehammer is docked on startup;
2013-08-17, by wenzelm
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
2013-08-17, by wenzelm
more robust startup;
2013-08-17, by wenzelm
some protocol to determine provers according to ML;
2013-08-17, by wenzelm
public access for protocol handlers and protocol commands -- to be used within reason;
2013-08-17, by wenzelm
always enable "minimize" to simplify interaction model;
2013-08-17, by wenzelm
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
2013-08-17, by wenzelm
recovered Locale.intern from d51bac27d4a0 (still used in AFP/Simp);
2013-08-17, by wenzelm
NEWS;
2013-08-17, by wenzelm
eliminated pointless subgoal argument;
2013-08-17, by wenzelm
more direct sledgehammer configuration via mode = Normal_Result and output_result;
2013-08-17, by wenzelm
more explicit sendback propertries based on mode;
2013-08-17, by wenzelm
tuned;
2013-08-16, by wenzelm
check_tool wrt. official ISABELLE_TOOLS;
2013-08-16, by wenzelm
more markup via Name_Space.check;
2013-08-16, by wenzelm
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
2013-08-16, by wenzelm
standardized aliases;
2013-08-16, by wenzelm
more markup -- avoid old Locale.extern;
2013-08-16, by wenzelm
renamed function
2013-08-16, by blanchet
eliminate quasi-duplicate function
2013-08-16, by blanchet
generalized "mk_permute"
2013-08-16, by blanchet
tuning
2013-08-16, by blanchet
added more functions to BNF library
2013-08-16, by blanchet
moved function to where it seems to belong
2013-08-16, by blanchet
moved library function where it belongs, and used Dmitriy's inside-out implementation
2013-08-16, by blanchet
added useful library function
2013-08-16, by blanchet
tuned
2013-08-16, by traytel
moved useful library functions upstream
2013-08-16, by blanchet
merge
2013-08-16, by blanchet
added fixme
2013-08-14, by blanchet
more (co)datatype documentation
2013-08-14, by blanchet
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
2013-08-14, by Andreas Lochbihler
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
2013-08-13, by traytel
more work on (co)datatype docs
2013-08-14, by blanchet
more symbolic notation;
2013-08-13, by wenzelm
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
2013-08-13, by wenzelm
merged
2013-08-13, by wenzelm
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
2013-08-13, by wenzelm
merged
2013-08-13, by wenzelm
more general window_geometry;
2013-08-13, by wenzelm
added rail diagram
2013-08-13, by blanchet
merged
2013-08-13, by wenzelm
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-13, by wenzelm
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-08-13, by wenzelm
imported patch added_e_1_8
2013-08-13, by blanchet
remove unnecessary dependencies on Library/Quotient_*
2013-08-13, by kuncar
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-08-13, by kuncar
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
2013-08-13, by kuncar
move useful lemmas to Main
2013-08-13, by kuncar
merged
2013-08-13, by wenzelm
indicate error-functions more prominently (by name prefix instead of suffix);
2013-08-09, by Christian Sternagel
avoid low-level Same structure;
2013-08-09, by Christian Sternagel
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip