isabelle: Graph

simplified via Position extractors;
2010-05-05, by wenzelm
some rearrangement of Scala sources;
2010-05-05, by wenzelm
fminus and some more theorems ported from Finite_Set.
2010-05-05, by Cezary Kaliszyk
eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05, by haftmann
tuned whitespace
2010-05-05, by haftmann
tuned interpunctation, dropped dead comment
2010-05-05, by haftmann
merged
2010-05-04, by huffman
avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)
2010-05-04, by huffman
generalize some lemmas to class t1_space
2010-05-04, by huffman
simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04, by huffman
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
return updated info record after termination proof
2010-04-30, by krauss
proper context for rule_by_tactic;
2010-04-30, by wenzelm
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
2010-04-30, by wenzelm
hgweb style: show author in filelog; full description in annotate hover
2010-04-29, by krauss
proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29, by wenzelm
read_const: disallow internal names as usual in visible Isar text;
2010-04-29, by wenzelm
more explicit treatment of context, although not fully localized;
2010-04-29, by wenzelm
removed some Emacs junk;
2010-04-29, by wenzelm
merged
2010-04-29, by haftmann
make random engine persistent using code_reflect
2010-04-29, by haftmann
repaired subtle misunderstanding: statement names are only passed for name resolution
2010-04-29, by haftmann
fixed underscore typo
2010-04-29, by haftmann
more coherent naming with ML serializer
2010-04-29, by haftmann
dropped code_datatype antiquotation
2010-04-29, by haftmann
dropped unnecessary ML code
2010-04-29, by haftmann
avoid popular infixes
2010-04-29, by haftmann
code_reflect: specify module name directly after keyword
2010-04-29, by haftmann
NEWS: code_reflect
2010-04-29, by haftmann
merged
2010-04-29, by haftmann
updated generated file
2010-04-28, by haftmann
modernized structure name
2010-04-28, by haftmann
use code_reflect
2010-04-28, by haftmann
merged
2010-04-29, by wenzelm
Tuning the quotient examples
2010-04-29, by Cezary Kaliszyk
clarified signature; simpler implementation in terms of function's tactic interface
2010-04-28, by krauss
return info record (relative to auxiliary context!)
2010-04-28, by krauss
default termination prover as plain tactic
2010-04-28, by krauss
function: sane interface for programmatic use
2010-04-28, by krauss
ML interface uses plain command names, following conventions from typedef
2010-04-28, by krauss
function: better separate Isar integration from actual functionality
2010-04-28, by krauss
merged
2010-04-29, by haftmann
export somehow odd mapa explicitly
2010-04-28, by haftmann
exported print_tuple
2010-04-28, by haftmann
take into account tupled constructors
2010-04-28, by haftmann
avoid code_datatype antiquotation
2010-04-28, by haftmann
merged
2010-04-28, by bulwahn
added an example with a free function variable to the Predicate Compile examples
2010-04-28, by bulwahn
removed local clone in the predicate compiler
2010-04-28, by bulwahn
improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
2010-04-28, by bulwahn
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
2010-04-29, by wenzelm
'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29, by wenzelm
adapted ProofContext.infer_type;
2010-04-29, by wenzelm
ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-29, by wenzelm
avoid clash with keyword 'write';
2010-04-29, by wenzelm
allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-29, by wenzelm
uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
2010-04-29, by wenzelm
disabled spurious invocation of (interactive) sledgehammer;
2010-04-28, by wenzelm
merged
2010-04-28, by wenzelm
make Mirabelle happy
2010-04-28, by blanchet
remove removed option
2010-04-28, by blanchet
merge
2010-04-28, by blanchet
parentheses around nested cases
2010-04-28, by blanchet
merged
2010-04-28, by blanchet
add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
2010-04-28, by blanchet
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
2010-04-28, by blanchet
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
2010-04-28, by blanchet
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28, by blanchet
redo Sledgehammer proofs (and get rid of "neg_clausify")
2010-04-28, by blanchet
removed "sorts" option, continued
2010-04-28, by blanchet
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
2010-04-28, by blanchet
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
2010-04-28, by blanchet
support Vampire definitions of constants as "let" constructs in Isar proofs
2010-04-28, by blanchet
tuning
2010-04-27, by blanchet
redid the proofs with the latest Sledgehammer;
2010-04-27, by blanchet
remove Nitpick functions that are now implemented in Sledgehammer
2010-04-27, by blanchet
added total goal count as argument + message when killing ATPs
2010-04-27, by blanchet
make Sledgehammer more friendly if no subgoal is left
2010-04-27, by blanchet
polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs
2010-04-27, by blanchet
reintroduce missing "gen_all_vars" call
2010-04-27, by blanchet
fix types of "fix" variables to help proof reconstruction and aid readability
2010-04-27, by blanchet
allow schematic variables in types in terms that are reconstructed by Sledgehammer
2010-04-27, by blanchet
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
2010-04-27, by blanchet
new Isar proof construction code: stringfy axiom names correctly
2010-04-27, by blanchet
honor "shrink_proof" Sledgehammer option
2010-04-27, by blanchet
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-27, by blanchet
updated keywords
2010-04-28, by haftmann
exported cert_tyco, read_tyco
2010-04-28, by haftmann
added code_reflect command
2010-04-28, by haftmann
merged
2010-04-28, by haftmann
fix "fors" for proof of monotonicity
2010-04-28, by haftmann
merge
2010-04-28, by Cezary Kaliszyk
merge
2010-04-28, by Cezary Kaliszyk
Tuned FSet
2010-04-28, by Cezary Kaliszyk
merged
2010-04-28, by haftmann
try to observe intended meaning of add_registration interface more closely
2010-04-28, by haftmann
codified comment
2010-04-28, by haftmann
merged
2010-04-28, by haftmann
empty class specifcations observe default sort
2010-04-28, by haftmann
document some known problems with Mac OS;
2010-04-28, by wenzelm
removed redundant/ignored sort constraint;
2010-04-28, by wenzelm
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
2010-04-28, by wenzelm
made SML/NJ happy;
2010-04-28, by wenzelm
updated keywords;
2010-04-28, by wenzelm
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
2010-04-28, by wenzelm
removed material that is out of scope of this manual;
2010-04-28, by wenzelm
renamed command 'defaultsort' to 'default_sort';
2010-04-28, by wenzelm
localized default sort;
2010-04-28, by wenzelm
more systematic naming of tsig operations;
2010-04-28, by wenzelm
modernized/simplified Sign.set_defsort;
2010-04-28, by wenzelm
get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
2010-04-28, by wenzelm
export Type.minimize_sort;
2010-04-28, by wenzelm
term_typ: print styled term
2010-04-28, by haftmann
merged
2010-04-27, by wenzelm
merged
2010-04-27, by huffman
generalize types of path operations
2010-04-27, by huffman
generalize more continuity lemmas
2010-04-27, by huffman
generalized many lemmas about continuity
2010-04-27, by huffman
simplify definition of continuous_on; generalize some lemmas
2010-04-26, by huffman
move intervals section heading
2010-04-26, by huffman
remove unused, redundant constant inv_on
2010-04-26, by huffman
reorganize subsection headings
2010-04-26, by huffman
remove redundant lemma
2010-04-26, by huffman
more lemmas to Vec1.thy
2010-04-26, by huffman
simplify proof
2010-04-26, by huffman
move more lemmas into Vec1.thy
2010-04-26, by huffman
move proof of Fashoda meet theorem into separate file
2010-04-26, by huffman
move definitions and theorems for type real^1 to separate theory file
2010-04-26, by huffman
removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27, by wenzelm
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27, by wenzelm
really minimize sorts after certification -- looks like this is intended here;
2010-04-27, by wenzelm
tuned signature;
2010-04-27, by wenzelm
merged
2010-04-27, by wenzelm
tuned whitespace
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
fix SML/NJ compilation (I hope)
2010-04-27, by blanchet
tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27, by wenzelm
tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27, by wenzelm
tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27, by wenzelm
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27, by wenzelm
misc tuning and simplification;
2010-04-27, by wenzelm
NEWS and CONTRIBUTORS
2010-04-27, by haftmann
explicit is better than implicit
2010-04-27, by haftmann
tuned class linordered_field_inverse_zero
2010-04-27, by haftmann
merged
2010-04-27, by haftmann
instances for *_inverse_zero classes
2010-04-27, by haftmann
canonical import
2010-04-27, by haftmann
merged
2010-04-26, by haftmann
use new classes (linordered_)field_inverse_zero
2010-04-26, by haftmann
merged
2010-04-26, by blanchet
renamed option
2010-04-26, by blanchet
fixes 2a5c6e7b55cb;
2010-04-26, by blanchet
compile
2010-04-26, by blanchet
make compile (and not just load dynamically)
2010-04-26, by blanchet
merge
2010-04-26, by blanchet
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
2010-04-26, by blanchet
adapt code to reflect new signature of "neg_clausify"
2010-04-26, by blanchet
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
2010-04-26, by blanchet
rename options
2010-04-26, by blanchet
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
2010-04-26, by blanchet
remove needless code that was copy-pasted from Quickcheck (where it made sense)
2010-04-26, by blanchet
cosmetics
2010-04-25, by blanchet
cosmetics
2010-04-25, by blanchet
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-25, by blanchet
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-25, by blanchet
cosmetics: rename internal functions
2010-04-25, by blanchet
cosmetics
2010-04-25, by blanchet
remove "show_skolems" option and change style of record declarations
2010-04-25, by blanchet
remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-25, by blanchet
removed Nitpick's "uncurry" option
2010-04-24, by blanchet
fix typesetting
2010-04-24, by blanchet
Fruhjahrsputz: remove three mostly useless Nitpick options
2010-04-24, by blanchet
remove type annotations as comments;
2010-04-24, by blanchet
cosmetics
2010-04-24, by blanchet
better error reporting;
2010-04-24, by blanchet
cosmetics
2010-04-23, by blanchet
reuse timestamp function
2010-04-23, by blanchet
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-23, by blanchet
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
2010-04-23, by blanchet
remove some bloat
2010-04-23, by blanchet
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23, by blanchet
renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23, by blanchet
move the minimizer to the Sledgehammer directory
2010-04-23, by blanchet
remove debugging code
2010-04-23, by blanchet
move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23, by blanchet
give an error if no ATP is set
2010-04-23, by blanchet
move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-23, by blanchet
centralized ATP-specific error handling in "atp_wrapper.ML"
2010-04-23, by blanchet
handle ATP proof delimiters in a cleaner, more extensible fashion
2010-04-23, by blanchet
merged
2010-04-26, by wenzelm
fix another if-then-else parse error
2010-04-26, by huffman
fix if-then-else parse error
2010-04-26, by huffman
merged
2010-04-26, by huffman
fix syntax precedence declarations for UNION, INTER, SUP, INF
2010-04-26, by huffman
syntax precedence for If and Let
2010-04-26, by huffman
fix lots of looping simp calls and other warnings
2010-04-26, by huffman
fix duplicate simp rule warnings
2010-04-25, by huffman
define finer-than ordering on net type; move some theorems into Limits.thy
2010-04-25, by huffman
generalize type of continuous_on
2010-04-25, by huffman
define nets directly as filters, instead of as filter bases
2010-04-25, by huffman
use 'example_proof' (invisible);
2010-04-26, by wenzelm
command 'example_proof' opens an empty proof body;
2010-04-26, by wenzelm
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
2010-04-26, by wenzelm
eliminanated some unreferenced identifiers;
2010-04-26, by wenzelm
merged
2010-04-26, by wenzelm
add bounded_lattice_bot and bounded_lattice_top type classes
2010-04-26, by Cezary Kaliszyk
merged
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps
2010-04-26, by haftmann
class division_ring_inverse_zero
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-26, by haftmann
line break
2010-04-26, by haftmann
removed unused AxClass.class_intros;
2010-04-26, by wenzelm
updated Sign.add_type_abbrev;
2010-04-26, by wenzelm
merged
2010-04-26, by haftmann
field_simps as named theorems
2010-04-25, by haftmann
merged
2010-04-25, by wenzelm
generalize more constants and lemmas
2010-04-25, by huffman
simplify types of path operations (use real instead of real^1)
2010-04-25, by huffman
add lemmas convex_real_interval and convex_box
2010-04-25, by huffman
generalize more constants and lemmas
2010-04-24, by huffman
generalize constant closest_point
2010-04-24, by huffman
minimize imports
2010-04-24, by huffman
fix imports
2010-04-24, by huffman
document generation for Multivariate_Analysis
2010-04-24, by huffman
move l2-norm stuff into separate theory file
2010-04-24, by huffman
convert proofs to Isar-style
2010-04-24, by huffman
Library/Fraction_Field.thy: ordering relations for fractions
2010-04-24, by huffman
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-04-25, by wenzelm
more systematic treatment of data -- avoid slightly odd nested tuples here;
2010-04-25, by wenzelm
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25, by wenzelm
misc tuning and simplification;
2010-04-25, by wenzelm
simplified some private bindings;
2010-04-25, by wenzelm
classrel and arity completion by krauss/schropp;
2010-04-25, by wenzelm
removed obsolete/unused Proof.match_bind;
2010-04-25, by wenzelm
modernized naming conventions of main Isar proof elements;
2010-04-25, by wenzelm
goals: simplified handling of implicit variables -- removed obsolete warning;
2010-04-25, by wenzelm
updated generated files;
2010-04-23, by wenzelm
cover 'schematic_lemma' etc.;
2010-04-23, by wenzelm
mark schematic statements explicitly;
2010-04-23, by wenzelm
eliminated spurious schematic statements;
2010-04-23, by wenzelm
explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-23, by wenzelm
collapse category "schematic goal" in keyword table -- Proof General does not know about this;
2010-04-23, by wenzelm
added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-04-23, by wenzelm
merged
2010-04-23, by wenzelm
merged
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23, by haftmann
adapted to new times_divide_eq simp situation
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
less special treatment of times_divide_eq [simp]
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-23, by haftmann
more localization; tuned proofs
2010-04-23, by haftmann
more localization; factored out lemmas for division_ring
2010-04-23, by haftmann
modernized abstract algebra theories
2010-04-23, by haftmann
merged
2010-04-23, by haftmann
swapped generic code generator and SML code generator
2010-04-22, by haftmann
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
2010-04-23, by wenzelm
Item_Net/Named_Thms: export efficient member operation;
2010-04-23, by wenzelm
initialized atps reference with standard setup in the atp manager
2010-04-23, by bulwahn
compile
2010-04-23, by blanchet
handle SPASS's equality predicate correctly in Isar proof reconstruction
2010-04-23, by blanchet
merged
2010-04-23, by blanchet
added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs;
2010-04-23, by blanchet
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
2010-04-22, by blanchet
set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
2010-04-22, by blanchet
minor code cleanup
2010-04-22, by blanchet
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
2010-04-22, by blanchet
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
2010-04-22, by blanchet
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
2010-04-22, by blanchet
postprocess ATP output in "overlord" mode to make it more readable
2010-04-22, by blanchet
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
2010-04-21, by blanchet
generate command-line in addition to timestamp in ATP output file, for debugging purposes
2010-04-21, by blanchet
pass relevant options from "sledgehammer" to "sledgehammer minimize";
2010-04-21, by blanchet
Finite set theory
2010-04-23, by Cezary Kaliszyk
merged
2010-04-22, by wenzelm
Tidied up using s/l
2010-04-22, by paulson
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
2010-04-22, by wenzelm
fun_rel introduction and list_rel elimination for quotient package
2010-04-22, by Cezary Kaliszyk
lemmas concerning remdups
2010-04-22, by haftmann
lemma dlist_ext
2010-04-22, by haftmann
merged
2010-04-21, by haftmann
optionally ignore errors during translation of equations; tuned representation of abstraction points
2010-04-21, by haftmann
optionally ignore errors during translation of equations
2010-04-21, by haftmann
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
2010-04-21, by krauss
simplified example
2010-04-21, by krauss
use only one thread in "Manual_Nits";
2010-04-21, by blanchet
merged
2010-04-21, by blanchet
clarify error message
2010-04-21, by blanchet
distinguish between the different ATP errors in the user interface;
2010-04-21, by blanchet
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
2010-04-21, by blanchet
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
2010-04-20, by blanchet
merged
2010-04-21, by bulwahn
make profiling depend on reference Quickcheck.timing
2010-04-21, by bulwahn
added examples for detecting switches
2010-04-21, by bulwahn
adopting documentation of the predicate compiler
2010-04-21, by bulwahn
removing dead code; clarifying function names; removing clone
2010-04-21, by bulwahn
adopting examples to changes in the predicate compiler
2010-04-21, by bulwahn
adopting quickcheck
2010-04-21, by bulwahn
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
2010-04-21, by bulwahn
added switch detection to the predicate compiler
2010-04-21, by bulwahn
added further inlining of boolean constants to the predicate compiler
2010-04-21, by bulwahn
adding more profiling to the predicate compiler
2010-04-21, by bulwahn
only add relevant predicates to the list of extra modes
2010-04-21, by bulwahn
switched off no_topmost_reordering
2010-04-21, by bulwahn
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
2010-04-21, by bulwahn
added option for specialisation to the predicate compiler
2010-04-21, by bulwahn
prefer functional modes of functions in the mode analysis
2010-04-21, by bulwahn
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-04-21, by bulwahn
merged
2010-04-21, by hoelzl
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
2010-04-21, by hoelzl
Translated remaining theorems about integration from HOL light.
2010-04-20, by himmelma
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
2010-04-21, by wenzelm
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-04-20, by huffman
Remove garbage.
2010-04-20, by ballarin
Remove garbage.
2010-04-20, by ballarin
recovered isabelle java, which was broken in ebfa4bb0d50f;
2010-04-20, by wenzelm
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
2010-04-20, by blanchet
merged
2010-04-20, by blanchet
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-20, by blanchet
merge
2010-04-20, by blanchet
cosmetics
2010-04-19, by blanchet
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
2010-04-19, by blanchet
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19, by blanchet
added warning about inconsistent context to Metis;
2010-04-19, by blanchet
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
2010-04-19, by blanchet
got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19, by blanchet
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19, by blanchet
don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19, by blanchet
allow "_" in TPTP names in debug mode
2010-04-19, by blanchet
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-19, by blanchet
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19, by blanchet
get rid of "List.foldl" + add timestamp to SPASS
2010-04-19, by blanchet
less ambitious settings for cygwin-poly;
2010-04-20, by wenzelm
respectfullness and preservation of map for identity quotients
2010-04-20, by Cezary Kaliszyk
respectfullness and preservation of function composition
2010-04-20, by Cezary Kaliszyk
eta-normalize the goal since the original theorem is atomized
2010-04-20, by Cezary Kaliszyk
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
2010-04-20, by wenzelm
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
2010-04-20, by wenzelm
merged
2010-04-20, by haftmann
more appropriate representation of valid positions for abstractors
2010-04-19, by haftmann
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19, by haftmann
update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-04-19, by wenzelm
tuned;
2010-04-19, by wenzelm
more platform information;
2010-04-19, by wenzelm
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
2010-04-19, by wenzelm
some updates on multi-platform support;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-19, by haftmann
polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-19, by wenzelm
less ambitious settings for cygwin-poly;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
more convenient equations for zip
2010-04-19, by haftmann
more platform info;
2010-04-17, by wenzelm
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
2010-04-17, by wenzelm
system properties determine the JVM platform, not the Isabelle one;
2010-04-17, by wenzelm
THIS_CYGWIN;
2010-04-17, by wenzelm
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
2010-04-17, by wenzelm
isatest: more robust treatment of remote files, less reliance on mounted file system;
2010-04-17, by wenzelm
merged
2010-04-17, by blanchet
added missing \n in output
2010-04-17, by blanchet
by default, don't try to start ATPs that aren't installed
2010-04-16, by blanchet
fiddle with Sledgehammer option syntax
2010-04-16, by blanchet
added timestamp to proof
2010-04-16, by blanchet
restore order of clauses in TPTP output;
2010-04-16, by blanchet
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
2010-04-16, by blanchet
output total time taken by Sledgehammer if "verbose" is set
2010-04-16, by blanchet
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16, by blanchet
reorganize Sledgehammer's relevance filter slightly
2010-04-16, by blanchet
tell the user that Sledgehammer kills its siblings
2010-04-16, by blanchet
updated keywords;
2010-04-16, by wenzelm
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-16, by wenzelm
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16, by wenzelm
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16, by wenzelm
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16, by wenzelm
allow syntax types within abbreviations;
2010-04-16, by wenzelm
modernized old-style type abbreviations;
2010-04-16, by wenzelm
modernized type abbreviations;
2010-04-16, by wenzelm
local type abbreviations;
2010-04-16, by wenzelm
merged
2010-04-16, by blanchet
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16, by blanchet
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-16, by blanchet
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15, by blanchet
make Sledgehammer's output more debugging friendly
2010-04-15, by blanchet
made SML/NJ happy;
2010-04-16, by wenzelm