isabelle: Graph

generalize some lemmas
2010-05-04, by huffman
convert comments to 'text' blocks
2010-05-04, by huffman
generalize more lemmas about limits
2010-05-04, by huffman
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-05-05, by krauss
merged
2010-05-04, by huffman
generalize types of LIMSEQ and LIM; generalize many lemmas
2010-05-04, by huffman
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
2010-05-04, by huffman
make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04, by huffman
adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-04, by huffman
declare cont_discrete_cpo [cont2cont]
2010-05-04, by huffman
remove unneeded constant Zseq
2010-05-03, by huffman
add lemmas eventually_nhds_metric and tendsto_mono
2010-05-03, by huffman
remove unneeded premise
2010-05-03, by huffman
add constants netmap and nhds
2010-05-03, by huffman
Merged.
2010-05-04, by ballarin
Provide internal function for printing a single interpretation.
2010-05-04, by ballarin
Explicitly manage export in dependencies.
2010-04-27, by ballarin
fixed proof (cf. edc381bf7200);
2010-05-04, by wenzelm
Corrected imports; better approximation of dependencies.
2010-05-04, by hoelzl
Add Convex to Library build
2010-05-04, by hoelzl
Removed unnecessary assumption
2010-05-04, by hoelzl
Translating lemmas from Finite_Set to FSet.
2010-05-04, by Cezary Kaliszyk
merged
2010-05-04, by wenzelm
merged
2010-05-04, by berghofe
Turned Sem into an inductive definition.
2010-05-04, by berghofe
Corrected handling of "for" parameters.
2010-05-04, by berghofe
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
2010-05-04, by berghofe
added lemma about irreflexivity of pointer inequality in Imperative_HOL
2010-05-04, by bulwahn
added function ffilter and some lemmas from Finite_Set to the FSet theory
2010-05-04, by bulwahn
merged
2010-05-04, by haftmann
avoid if on rhs of default simp rules
2010-05-04, by haftmann
avoid exception Empty on malformed goal
2010-05-04, by krauss
locale predicates of classes carry a mandatory "class" prefix
2010-05-04, by haftmann
a ring_div is a ring_1_no_zero_divisors
2010-05-04, by haftmann
NEWS
2010-05-04, by haftmann
merged
2010-05-03, by huffman
merged
2010-05-01, by huffman
complete_lattice instance for net type
2010-05-01, by huffman
swap ordering on nets, so x <= y means 'x is finer than y'
2010-05-01, by huffman
fixrec no longer uses global simpset internally to prove equations
2010-05-01, by huffman
move setsum lemmas to Product_plus.thy
2010-05-01, by huffman
remove duplicate lemmas
2010-04-30, by huffman
add lemmas about convergent
2010-04-30, by huffman
Cleanup information theory
2010-05-03, by hoelzl
Moved Convex theory to library.
2010-05-03, by hoelzl
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-20, by hoelzl
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04, by wenzelm
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04, by wenzelm
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-04, by wenzelm
specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
2010-05-04, by wenzelm
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
2010-05-03, by wenzelm
replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
2010-05-03, by wenzelm
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03, by wenzelm
minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03, by wenzelm
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-05-03, by wenzelm
old NEWS on global operations;
2010-05-03, by wenzelm
ProofContext.init_global;
2010-05-03, by wenzelm
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-05-03, by wenzelm
merged
2010-05-03, by haftmann
do not generate code per default -- touches file of parent session
2010-04-30, by haftmann
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-05-01, by krauss
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
2010-05-01, by krauss
now if this doesn't make SML/NJ happy, nothing will
2010-05-01, by blanchet
more stats;
2010-05-01, by wenzelm
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-30, by wenzelm
slightly more standard induct_simp_add/del attributes;
2010-04-30, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-30, by wenzelm
export Simplifier.with_context;
2010-04-30, by wenzelm
removed some old comments;
2010-04-30, by wenzelm
merged
2010-04-30, by huffman
merged
2010-04-30, by huffman
generalize lemma adjoint_unique; simplify some proofs
2010-04-29, by huffman
fix latex url
2010-04-29, by huffman
merged
2010-04-29, by huffman
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-29, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
2010-04-29, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
2010-04-29, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-29, by huffman
generalize LIMSEQ_vector to tendsto_vector
2010-04-28, by huffman
generalize orthogonal_clauses
2010-04-28, by huffman
remove redundant lemma vector_dist_norm
2010-04-28, by huffman
remove redundant lemma norm_0
2010-04-28, by huffman
generalize some euclidean space lemmas
2010-04-28, by huffman
prove lemma openin_subopen without using choice
2010-04-28, by huffman
move path-related stuff into new theory file
2010-04-28, by huffman
add new Multivariate_Analysis files to IsaMakefile
2010-04-28, by huffman
move operator norm stuff to new theory file
2010-04-28, by huffman
eliminated spurious sledgehammer invocation;
2010-04-30, by wenzelm
merged
2010-04-30, by wenzelm
merged
2010-04-30, by haftmann
merged
2010-04-30, by haftmann
enclose case expression in brackets
2010-04-30, by haftmann
catch the right exception
2010-04-30, by blanchet
eliminate trivial case splits from Isar proofs
2010-04-30, by blanchet
remove debugging code
2010-04-30, by blanchet
merged
2010-04-30, by blanchet
minor improvements
2010-04-30, by blanchet
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
2010-04-30, by blanchet
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
2010-04-30, by blanchet
in "overlord" mode: ignore problem prefix specified in the .thy file
2010-04-29, by blanchet
uncomment code
2010-04-29, by blanchet
redid some Sledgehammer/Metis proofs
2010-04-29, by blanchet
fix more "undeclared symbol" errors related to SPASS's DFG format
2010-04-29, by blanchet
be more discriminate: some one-line Isar proofs are silly
2010-04-29, by blanchet
one-step Isar proofs are not always pointless
2010-04-29, by blanchet
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
2010-04-29, by blanchet
redo more Metis/Sledgehammer example
2010-04-29, by blanchet
fixed definition of "bad frees" so that it actually works
2010-04-29, by blanchet
don't remove last line of proof
2010-04-29, by blanchet
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
2010-04-29, by blanchet
make SML/NJ happy, take 2
2010-04-29, by blanchet
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
2010-04-29, by blanchet
expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-29, by blanchet
more neg_clausify proofs that get replaced by direct proofs
2010-04-29, by blanchet
redo some of the metis proofs
2010-04-28, by blanchet
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
2010-04-28, by blanchet
improve unskolemization
2010-04-28, by blanchet
make sure short theorem names are preferred to composite ones in Sledgehammer;
2010-04-28, by blanchet
properly extract SPASS proof
2010-04-28, by blanchet
try out Vampire 11 and parse its output correctly;
2010-04-28, by blanchet