isabelle: Graph

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
more symbols;
2015-06-29, by wenzelm
corrected typo
2015-06-29, by nipkow
tuned src/HOL/ex/Ballot
2015-06-16, by hoelzl
add examples from Freek's top 100 theorems (thms 30, 73, 77)
2015-06-12, by bulwahn
generalized geometric distribution
2015-06-17, by hoelzl
added lemma
2015-06-28, by nipkow
simplified termination criterion for euclidean algorithm (again)
2015-06-27, by haftmann
tuned proof
2015-06-27, by haftmann
rings follow immediately their corresponding semirings
2015-06-27, by haftmann
tuned code setup
2015-06-27, by haftmann
algebraic specification for set gcd
2015-06-27, by haftmann
premises in 'show' are treated like 'assume';
2015-06-27, by wenzelm
adapted to a9b71c82647b;
2015-06-26, by wenzelm
merged
2015-06-26, by wenzelm
isabelle update_cartouches;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
tuned proofs;
2015-06-26, by wenzelm
do not expose goal parameters;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
proper spacing, as for other syntax for these symbols;
2015-06-26, by wenzelm
tuned whitespace;
2015-06-26, by wenzelm
updated SystemOnTPTP URL
2015-06-26, by blanchet
tuned proofs;
2015-06-26, by wenzelm
merged
2015-06-25, by wenzelm
implicit goal cases are legacy;
2015-06-25, by wenzelm
tuned proofs;
2015-06-25, by wenzelm
more heap -- hoping for more stability of HOL-Proofs;
2015-06-25, by wenzelm
added method "goals" for proper subgoal cases;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
tuned;
2015-06-25, by wenzelm
tuned;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
2015-06-25, by haftmann
euclidean algorithm on polynomials
2015-06-25, by haftmann
more theorems
2015-06-25, by haftmann
generalized to definition from literature, which covers also polynomials
2015-06-25, by haftmann
put E before (typically remote, hence less reliable) Vampire
2015-06-25, by blanchet
tuned proofs -- less digits;
2015-06-24, by wenzelm
updated to scala-2.11.7;
2015-06-24, by wenzelm
clarified 'case' command;
2015-06-24, by wenzelm
silence 'try'
2015-06-24, by blanchet
Merge
2015-06-23, by paulson
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-23, by paulson
tuned proofs;
2015-06-23, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
merged
2015-06-22, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
tuned;
2015-06-22, by wenzelm
support 'when' statement, which corresponds to 'presume';
2015-06-22, by wenzelm
added method "sleep";
2015-06-22, by wenzelm
tuned signature;
2015-06-22, by wenzelm
tuned whitespace;
2015-06-22, by wenzelm
clarified nesting of Isar goal structure;
2015-06-22, by wenzelm
tuned;
2015-06-22, by wenzelm
keep 'Pure.all' in goals when preplaying
2015-06-22, by blanchet
use right context for preplay, to avoid errors in fact lookup
2015-06-22, by blanchet