Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-448
+448
+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.
trim context for persistent storage;
2015-08-30, by wenzelm
tuned;
2015-08-30, by wenzelm
clarified implicit context;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
tuned documentation -- merge is implicitly performed by the system;
2015-08-28, by wenzelm
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
2015-08-28, by wenzelm
more abstract theory certificate, which is not necessarily the full theory;
2015-08-28, by wenzelm
eliminated obsolete environment variable
2015-08-28, by blanchet
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
clarified language context, e.g. relevant for symbols;
2015-08-28, by wenzelm
merged;
2015-08-28, by wenzelm
tuned;
2015-08-26, by wenzelm
generate proper error instead of exception if goal cannot be atomized
2015-08-27, by blanchet
standardized some occurences of ancient "split" alias
2015-08-27, by haftmann
more lemmas on sorting and multisets (due to Thomas Sewell)
2015-08-27, by haftmann
robust handling of Vampire 4 proofs
2015-08-27, by blanchet
reverted 6ac3172985d4 -- the old URL has been restored
2015-08-27, by blanchet
fixed typo in comment
2015-08-27, by blanchet
use fancy options of Java 8;
2015-08-26, by wenzelm
tuned signature;
2015-08-26, by wenzelm
clarified kill on Windows: just one executable;
2015-08-26, by wenzelm
avoid deprecated PluginOptions with its unbounded window size;
2015-08-25, by wenzelm
clarified undefined_blobs: already loaded theories are suppressed;
2015-08-25, by wenzelm
tuned spacing
2015-08-25, by nipkow
tuned exercise
2015-08-25, by nipkow
merged
2015-08-24, by wenzelm
reset focus after thread update (with new debug_states);
2015-08-24, by wenzelm
atomic Debugger.status;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
more thorough GUI update;
2015-08-24, by wenzelm
maintain per-thread focus context;
2015-08-24, by wenzelm
typos
2015-08-24, by nipkow
nex exercise
2015-08-24, by nipkow
more explicit debugger caret rendering;
2015-08-24, by wenzelm
more explicit type Debugger.Context;
2015-08-23, by wenzelm
more precise tree re-selection;
2015-08-23, by wenzelm
proper GUI event;
2015-08-23, by wenzelm
update focus more thoroughly;
2015-08-23, by wenzelm
tuned;
2015-08-22, by wenzelm
merged
2015-08-21, by traytel
don't use types that come from the database---they are inconsistent with the ones occurring in the terms
2015-08-21, by traytel
tuned;
2015-08-21, by wenzelm
clarified linux application bundle;
2015-08-21, by wenzelm
more version information;
2015-08-21, by wenzelm
separate bundle for windows64;
2015-08-21, by wenzelm
tuned;
2015-08-21, by wenzelm
more scalable GUI;
2015-08-21, by wenzelm
eliminated WinRun4J artifact;
2015-08-21, by wenzelm
proper classpath for launcher;
2015-08-21, by wenzelm
updated to jdk-8u60, with support for x86_64-windows;
2015-08-21, by wenzelm
updated to recent launch4j 3.8;
2015-08-21, by wenzelm
clarified modules;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
tuned signature, according to ML version;
2015-08-20, by wenzelm
The Stone-Weierstrass theorem
2015-08-20, by paulson
tuned;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
NEWS;
2015-08-20, by wenzelm
updated to polyml-5.5.3-20150820, with native x86-windows support;
2015-08-20, by wenzelm
precise BinIO, without newline conversion on Windows;
2015-08-20, by wenzelm
repaired proofs after 6a6f15d8fbc4;
2015-08-19, by wenzelm
merged
2015-08-19, by wenzelm
clarified x86-windows setup;
2015-08-19, by wenzelm
proper check for Windows executables;
2015-08-19, by wenzelm
Cygwin bash on Windows;
2015-08-19, by wenzelm
tuned;
2015-08-19, by wenzelm
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
2015-08-19, by wenzelm
New material and fixes related to the forthcoming Stone-Weierstrass development
2015-08-19, by paulson
disabled auto resolve, until practical consequences are more clear;
2015-08-19, by wenzelm
example options;
2015-08-18, by wenzelm
proper platform_path;
2015-08-18, by wenzelm
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
2015-08-18, by wenzelm
SOMEthing went wrong in eb87fc42825c;
2015-08-18, by wenzelm
include libgmp;
2015-08-18, by wenzelm
proper platform path for intial PolyML.SaveState.loadState;
2015-08-18, by wenzelm
proper platform path for initial load;
2015-08-18, by wenzelm
tuned signature;
2015-08-18, by wenzelm
keep native CInterface to make SHA1 work properly;
2015-08-18, by wenzelm
more setup for native Windows (Pure and HOL session with image);
2015-08-18, by wenzelm
basic setup for native Windows (RAW session without image);
2015-08-17, by wenzelm
more complete build;
2015-08-17, by wenzelm
support for native x86-windows via MinGW32;
2015-08-17, by wenzelm
no ML_debugger support in Pure -- too complicated;
2015-08-17, by wenzelm
more careful propagation of ML_debugger option to Pure;
2015-08-17, by wenzelm
support for ML files with/without debugger information;
2015-08-17, by wenzelm
explicit debug flag for ML compiler;
2015-08-17, by wenzelm
tuned;
2015-08-17, by wenzelm
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
2015-08-17, by wenzelm
clarified initial ML name space (amending 7aad4be8a48e);
2015-08-16, by wenzelm
produce certified vars without access to theory_of_thm, and without context;
2015-08-16, by wenzelm
produce certified vars without access to theory_of_thm, and without context;
2015-08-16, by wenzelm
tuned;
2015-08-16, by wenzelm
added Thm.chyps_of;
2015-08-16, by wenzelm
prefer theory_id operations;
2015-08-16, by wenzelm
separate type theory_id;
2015-08-16, by wenzelm
delete precisely the added rules;
2015-08-16, by wenzelm
clarified context;
2015-08-16, by wenzelm
tuned whitespace;
2015-08-16, by wenzelm
tuned signature;
2015-08-16, by wenzelm
tuned;
2015-08-16, by wenzelm
tuned whitespace;
2015-08-15, by wenzelm
tuned whitespace;
2015-08-15, by wenzelm
obsolete;
2015-08-15, by wenzelm
clarified context;
2015-08-15, by wenzelm
clarified context;
2015-08-15, by wenzelm
tuned GUI;
2015-08-15, by wenzelm
proper setup of evaluation context;
2015-08-15, by wenzelm
tuned;
2015-08-15, by wenzelm
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
2015-08-15, by wenzelm
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
2015-08-15, by wenzelm
tuned signature;
2015-08-15, by wenzelm
qualified adjust_*
2015-08-13, by haftmann
more lemmas
2015-08-13, by haftmann
unfold intermediate definitions (stemming from composition) in lifted bnf operations
2015-08-13, by traytel
merged
2015-08-13, by wenzelm
more standard options;
2015-08-13, by wenzelm
prefer official @{make_string};
2015-08-13, by wenzelm
tuned signature, in accordance to sortBy in Scala;
2015-08-13, by wenzelm
clarified modules;
2015-08-12, by wenzelm
tuned NEWS
2015-08-13, by traytel
actually process lift_bnf regression suite
2015-08-12, by traytel
NEWS, CONTRIBUTORS, documentation for lift_bnf
2015-08-12, by traytel
use lift_bnf in an example
2015-08-12, by traytel
new command for lifting BNF structure over typedefs
2015-08-12, by traytel
more thorough reload;
2015-08-12, by wenzelm
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
2015-08-12, by wenzelm
merged
2015-08-12, by wenzelm
tuned colors;
2015-08-12, by wenzelm
clarified breakpoint rendering;
2015-08-12, by wenzelm
clarified;
2015-08-12, by wenzelm
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
2015-08-12, by wenzelm
clarified init/exit vs. session phase;
2015-08-12, by wenzelm
clarify type vs. term instantiation when forming closure;
2015-08-12, by Daniel Matichuk
more accurate dependencies;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
clarified thread re-selection;
2015-08-11, by wenzelm
clarified tree row handling;
2015-08-11, by wenzelm
proper context (amending 7aad4be8a48e);
2015-08-11, by wenzelm
suppress threads without debug state;
2015-08-11, by wenzelm
clarified events;
2015-08-11, by wenzelm
clarified GUI event handling;
2015-08-11, by wenzelm
tuned signature;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
misc tuning and clarification;
2015-08-11, by wenzelm
print values for stack entry;
2015-08-11, by wenzelm
clarified output;
2015-08-11, by wenzelm
default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
2015-08-11, by wenzelm
clarified break *point* position;
2015-08-11, by wenzelm
support hyperlinks with optional focus change;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
vacuous input means continue, e.g. after exit;
2015-08-11, by wenzelm
GUI actions depend on active debugger;
2015-08-11, by wenzelm
init/exit depending on active debugger panels;
2015-08-11, by wenzelm
eliminated cancel operation: disrupts normal evaluation of thread;
2015-08-11, by wenzelm
register thread such that cancel works;
2015-08-11, by wenzelm
clarified default selection;
2015-08-10, by wenzelm
report final debugger_state more robustly, e.g. after interrupt;
2015-08-10, by wenzelm
eliminated global option: breakpoints control this individually;
2015-08-10, by wenzelm
more uniform ScrollPane, like graphview;
2015-08-10, by wenzelm
tuned signature;
2015-08-10, by wenzelm
tuned rendering;
2015-08-10, by wenzelm
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
2015-08-10, by wenzelm
more thorough Encode.string;
2015-08-10, by wenzelm
added action to toggle breakpoints (on editor side);
2015-08-10, by wenzelm
sort lines;
2015-08-10, by wenzelm
rendering for debugger/breakpoint active state;
2015-08-10, by wenzelm
follow debugger focus;
2015-08-10, by wenzelm
tuned signature;
2015-08-10, by wenzelm
tuned imports;
2015-08-10, by wenzelm
tuned messages;
2015-08-10, by wenzelm
clarified ML options;
2015-08-10, by wenzelm
merged
2015-08-08, by wenzelm
more single stepping;
2015-08-08, by wenzelm
direct bootstrap of integer division from natural division
2015-08-08, by haftmann
slight cleanup of lemmas
2015-08-06, by haftmann
obsolete since no code generator without dictionary construction left
2015-08-06, by haftmann
make SML/NJ work;
2015-08-07, by wenzelm
suppress empty messages as usual;
2015-08-07, by wenzelm
proper Symbol.decode/encode;
2015-08-07, by wenzelm
eval ML context;
2015-08-07, by wenzelm
maintain history more often;
2015-08-07, by wenzelm
approximate old selection after update;
2015-08-06, by wenzelm
expand all rows for robustness and simplicity;
2015-08-06, by wenzelm
evaluate ML expressions within debugger context;
2015-08-06, by wenzelm
clarified debugger loop;
2015-08-06, by wenzelm
clarified thread state;
2015-08-06, by wenzelm
tuned;
2015-08-06, by wenzelm
more controls;
2015-08-06, by wenzelm
tuned;
2015-08-06, by wenzelm
clarified signature, to make debugger.ML compile with current official ML versions;
2015-08-06, by wenzelm
support for tree selection;
2015-08-05, by wenzelm
proper dynamic update;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
more GUI components;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
more controls;
2015-08-05, by wenzelm
proper initialization;
2015-08-05, by wenzelm
tuned signature;
2015-08-05, by wenzelm
protocol support for thread debugger state;
2015-08-05, by wenzelm
eliminated clone;
2015-08-04, by wenzelm
merged
2015-08-04, by wenzelm
more symbols;
2015-08-04, by wenzelm
more symbols;
2015-08-04, by wenzelm
more documentation of coercions
2015-08-04, by traytel
merged
2015-07-30, by wenzelm
clarified management of (single) session;
2015-07-30, by wenzelm
maintain debugger output messages;
2015-07-30, by wenzelm
provide CharSequence operations as well;
2015-07-30, by wenzelm
more GUI components;
2015-07-29, by wenzelm
tuned;
2015-07-29, by wenzelm
separate channel for debugger output;
2015-07-29, by wenzelm
clarified thread name;
2015-07-29, by wenzelm
add coinduction rule for infinite
2015-07-30, by Andreas Lochbihler
merged
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
more explicit context;
2015-07-28, by wenzelm
eliminated dead code;
2015-07-28, by wenzelm
clarified Variable.gen_all;
2015-07-28, by wenzelm
more explicit context;
2015-07-28, by wenzelm
more direct access to atomic cterms;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
proper context;
2015-07-28, by wenzelm
more direct access to atomic cterms;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
merged
2015-07-28, by immler
merged
2015-07-28, by immler
added theory Uniform_Limit
2015-07-28, by immler
evade timeout problem on macbroy6 (potentially due to NFS oddities);
2015-07-28, by wenzelm
tweaks. Got rid of a really slow step
2015-07-28, by paulson
the Cauchy integral theorem and related material
2015-07-28, by paulson
depth -> height; removed del_rightmost (too specifi)
2015-07-28, by nipkow
tuned;
2015-07-27, by wenzelm
merged
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
formal class for factorial (semi)rings
2015-07-27, by haftmann
merged
2015-07-27, by wenzelm
NEWS;
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
New material for Cauchy's integral theorem
2015-07-27, by paulson
tuned signature for print_nested_cases;
2015-07-27, by wenzelm
more explicit checks -- improved errors;
2015-07-27, by wenzelm
eliminated cterm_instantiate;
2015-07-27, by wenzelm
updated to infer_instantiate;
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
2015-07-27, by wenzelm
eliminated atac, rtac, etac, dtac, ftac;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
proper context;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
ignore non-existant variables, like other instantiate rules;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
added infer_instantiate';
2015-07-26, by wenzelm
more uniform exceptions, like cterm_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-25, by wenzelm
more accurate maxidx;
2015-07-25, by wenzelm
clarified error;
2015-07-25, by wenzelm
added infer_instantiate, which is meant to supersede cterm_instantiate;
2015-07-25, by wenzelm
eliminated alias;
2015-07-24, by wenzelm
proper context;
2015-07-24, by wenzelm
unused;
2015-07-24, by wenzelm
proper context;
2015-07-24, by wenzelm
more symbols by default, without xsymbols mode;
2015-07-23, by wenzelm
Measures form a CCPO
2015-07-23, by hoelzl
reorganized Extended_Real
2015-07-23, by hoelzl
isabelle update_cartouches;
2015-07-23, by wenzelm
tuned proofs;
2015-07-23, by wenzelm
proper latex;
2015-07-23, by wenzelm
tuned proofs;
2015-07-22, by wenzelm
tuned proofs;
2015-07-22, by wenzelm
support for ML debugger;
2015-07-21, by wenzelm
more explicit thread identification;
2015-07-21, by wenzelm
avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes;
2015-07-21, by wenzelm
new material for multivariate analysis, etc.
2015-07-20, by paulson
proper LaTeX;
2015-07-20, by wenzelm
updated to jdk-8u51;
2015-07-19, by wenzelm
more symbols;
2015-07-19, by wenzelm
isabelle update_cartouches;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
merged
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
tuned whitespace;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
reactivated dead code;
2015-07-18, by wenzelm
more uniform ComponentAdapter;
2015-07-17, by wenzelm
skeleton for interactive debugger;
2015-07-17, by wenzelm
tuned;
2015-07-17, by wenzelm
tuned;
2015-07-17, by wenzelm
store breakpoints within ML environment;
2015-07-17, by wenzelm
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
2015-07-17, by wenzelm
report possible breakpoint positions;
2015-07-17, by wenzelm
proper attribute;
2015-07-17, by wenzelm
forgotten selector
2015-07-17, by traytel
made code less loopy
2015-07-16, by blanchet
keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)
2015-07-16, by blanchet
generalized generic translation function
2015-07-16, by blanchet
merge
2015-07-16, by blanchet
tuning
2015-07-16, by blanchet
generalized limitation in documentation
2015-07-16, by blanchet
made tactic more robust w.r.t. equations containing 'case_prod'
2015-07-16, by blanchet
merged
2015-07-16, by wenzelm
merged
2015-07-16, by wenzelm
clarified boundary cases of completion;
2015-07-16, by wenzelm
additional ML parse tree components for Poly/ML 5.5.3, or later;
2015-07-16, by wenzelm
added option ML_debugger;
2015-07-16, by wenzelm
ML debugger interface;
2015-07-16, by wenzelm
{r,e,d,f}tac with proper context in BNF
2015-07-16, by traytel
move disjoint sets to their own theory
2015-07-16, by hoelzl
back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);
2015-07-15, by wenzelm
merged
2015-07-14, by wenzelm
more explicit command-line option for isabelle build;
2015-07-14, by wenzelm
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
2015-07-14, by wenzelm
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
2015-07-14, by wenzelm
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-07-14, by hoelzl
add continuous_onI_mono
2015-07-14, by hoelzl
tuned description
2015-07-13, by blanchet
tuning
2015-07-13, by blanchet
updated Isabelle description to CASC
2015-07-13, by blanchet
imported patch up_casc
2015-07-13, by blanchet
add emeasure_add_AE
2015-07-13, by hoelzl
stronger induction assumption in lfp_transfer and emeasure_lfp
2015-07-13, by hoelzl
refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h;
2015-07-13, by wenzelm
Quickcheck setup for finite sets
2015-07-12, by Lars Hupel
tuned proofs;
2015-07-11, by wenzelm
tuned proofs;
2015-07-11, by wenzelm
merged
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-09, by wenzelm
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
2015-07-09, by wenzelm
tuned whitespace;
2015-07-09, by wenzelm
tuned ML signature (and rationalized code a bit)
2015-07-09, by blanchet
merged
2015-07-09, by noschinl
case_of_simps: do not split for types with a single constructor
2015-07-09, by noschinl
tests for Simps_Case_Conv
2015-07-09, by noschinl
merged
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
clarified context;
2015-07-08, by wenzelm
Variable.focus etc.: optional bindings provided by user;
2015-07-08, by wenzelm
clarified text folds: proof ... qed counts as extra block;
2015-07-08, by wenzelm
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-07-08, by wenzelm
tuned;
2015-07-08, by wenzelm
tuned according to a81dc82ecba3;
2015-07-08, by wenzelm
tuned facts
2015-07-08, by haftmann
more cautious use of [iff] declarations
2015-07-08, by haftmann
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-08, by haftmann
eliminated some duplication
2015-07-08, by haftmann
more algebraic properties for gcd/lcm
2015-07-08, by haftmann
moved normalization and unit_factor into Main HOL corpus
2015-07-08, by haftmann
more generous timeout for the sake of HOL-Proofs in at64-poly;
2015-07-08, by wenzelm
tuned ML signature
2015-07-07, by blanchet
have the installed termination prover take a 'quiet' flag
2015-07-07, by blanchet
add monotonicity rule for rtranclp
2015-07-07, by hoelzl
tuned proofs;
2015-07-07, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
plain string output, without funny control chars;
2015-07-06, by wenzelm
tuned message;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
proper outer syntax category, e.g. relevant for PIDE markup;
2015-07-06, by wenzelm
merged
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified section references;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
removed outdated and mostly obsolete material;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified context;
2015-07-05, by wenzelm
obsolete;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
eliminated spurious warning/tracing messages -- avoid Display.string_of_thm_without_context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-07-05, by wenzelm
clarified context;
2015-07-03, by wenzelm
tuned signature;
2015-07-03, by wenzelm
clarified context;
2015-07-03, by wenzelm
tuned signature;
2015-07-03, by wenzelm
generalized sup_continuty of add, ereal_of_enat
2015-07-03, by hoelzl
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-07-03, by hoelzl
moved to lxbroy3, hoping that it works better;
2015-07-02, by wenzelm
separate (semi)ring with normalization
2015-07-02, by haftmann
merged
2015-07-02, by wenzelm
more CONTRIBUTORS;
2015-07-02, by wenzelm
documentation for 'subgoal' command;
2015-07-02, by wenzelm
clarified module;
2015-07-02, by wenzelm
allow to specify suffix of goal parameters;
2015-07-02, by wenzelm
subgoal parameters are internal by default and named by user;
2015-07-02, by wenzelm
split multi-goals as usual (outermost Pure.conjunction only);
2015-07-01, by wenzelm
clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
2015-07-01, by wenzelm
proper state after qed;
2015-07-01, by wenzelm
clarified keyword categories;
2015-07-01, by wenzelm
support for subgoal focus command;
2015-07-01, by wenzelm
tuned;
2015-07-01, by wenzelm
taylor series with has_integral and integrable_on
2015-07-01, by immler
merged
2015-06-30, by wenzelm
no arguments for "standard" (or old "default") methods;
2015-06-30, by wenzelm
renamed "default" to "standard", to make semantically clear what it is;
2015-06-30, by wenzelm
tuned;
2015-06-30, by wenzelm
Merge
2015-06-30, by paulson
Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-06-30, by paulson
generalized inf and sup_continuous; added intro rules
2015-06-30, by hoelzl
fix tex-output for rel_mset
2015-06-30, by hoelzl
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
2015-06-29, by blanchet
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
2015-06-29, by wenzelm
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-06-29, by wenzelm
clarified static phase;
2015-06-29, by wenzelm
tuned proofs;
2015-06-29, by wenzelm
more symbols;
2015-06-29, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-448
+448
+1000
+3000
+10000
tip