isabelle: Graph

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