isabelle: Graph

updated bib;
2009-09-15, by wenzelm
count number of iterations required for minimization (and fixed bug: minimization was always called)
2009-09-14, by nipkow
merged
2009-09-14, by haftmann
more antiquotations
2009-09-14, by haftmann
some lemmas about strict order in lattices
2009-09-14, by haftmann
explicitly export type abbreviations (as usual in SML97);
2009-09-13, by wenzelm
wrapper for Real.fmt -- via StringCvt.realfmt;
2009-09-13, by wenzelm
made SML/NJ happy;
2009-09-13, by wenzelm
standard headers and text sections;
2009-09-12, by wenzelm
merged
2009-09-11, by nipkow
Made record parameter flexible to allow for extensions
2009-09-11, by nipkow
merged
2009-09-11, by haftmann
corrected upper/lowercase
2009-09-11, by haftmann
merged
2009-09-10, by haftmann
obey underscore naming convention
2009-09-10, by haftmann
plain structure name; signature constraint; shorter lines
2009-09-10, by haftmann
split of test examples from NatTransfer
2009-09-10, by haftmann
generic transfer procedure
2009-09-10, by haftmann
early bootstrap of generic transfer procedure
2009-09-10, by haftmann
cleanedup theorems all_nat ex_nat
2009-09-10, by haftmann
atp_minimize is now not using whitelist
2009-09-10, by Philipp Meyer
position information is now passed to all actions;
2009-09-10, by nipkow
logging number of metis lemmas
2009-09-10, by nipkow
minimization: comparing w/ and w/o.
2009-09-09, by nipkow
merged
2009-09-09, by haftmann
dropped accidental code additions
2009-09-09, by haftmann
merged
2009-09-09, by haftmann
explicit transfer avoids spurious merge problems
2009-09-09, by haftmann
moved eq handling in nbe into separate oracle
2009-09-09, by haftmann
tuned document -- proper text instead of source comments, reduced line length;
2009-09-08, by wenzelm
fixed cleanup routine in neos csdp script
2009-09-01, by Philipp Meyer
timeout option for ATPs
2009-09-08, by boehmes
merged
2009-09-07, by wenzelm
modernized Event_Bus -- based on actors;
2009-09-07, by wenzelm
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
2009-09-07, by nipkow
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
Fixed a few problems with the method metisFT
2009-09-07, by paulson
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
2009-09-07, by paulson
merged
2009-09-07, by paulson
conflict resolution possibly
2009-09-07, by paulson
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
2009-09-04, by paulson
merged
2009-08-28, by paulson
More streamlining using metis.
2009-08-27, by paulson
enabled metis permanently, tuned stats
2009-09-07, by nipkow
added signature ATP_MINIMAL,
2009-09-05, by boehmes
merged
2009-09-05, by boehmes
separate output of ATP user time and sledgehammer (ML code) user time
2009-09-05, by boehmes
Mirabelle: command-line action options may either be key=value or just key
2009-09-05, by boehmes
added initialization and cleanup of actions,
2009-09-05, by boehmes
merged
2009-09-04, by haftmann
tuned metis proofs
2009-09-04, by haftmann
tuned
2009-09-04, by boehmes
tuned output
2009-09-04, by nipkow
merged
2009-09-03, by boehmes
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
2009-09-03, by boehmes
merged
2009-09-03, by haftmann
merged
2009-09-03, by haftmann
proper class syntax for sublocale class < expr
2009-09-03, by haftmann
added option full_typed for sledgehammer action
2009-09-03, by boehmes
added runtime information to sledgehammer
2009-09-03, by boehmes
tuned
2009-09-03, by boehmes
scaled avg_time
2009-09-03, by nipkow
merged
2009-09-03, by nipkow
tuned
2009-09-03, by nipkow
isatest: collect test results and logs in testdata repository
2009-09-03, by krauss
replaced backlist by whitelist
2009-09-03, by boehmes
Mirabelle: logging of exceptions (works only for PolyML)
2009-09-03, by boehmes
merged
2009-09-02, by wenzelm
refined delay into delay_first/delay_last;
2009-09-02, by wenzelm
merged
2009-09-02, by boehmes
add report script for Mirabelle
2009-09-02, by boehmes
Mirabelle: actions are responsible for handling exceptions,
2009-09-02, by boehmes
removed errors overseen in previous changes
2009-09-02, by boehmes
moved Mirabelle from HOL/Tools to HOL,
2009-09-02, by boehmes
removed unused signature
2009-09-02, by boehmes
explicit checks;
2009-09-02, by wenzelm
updated Poly/ML SVN version;
2009-09-02, by wenzelm
eval/location_props: always produce YXML markup, independent of print_mode;
2009-09-02, by wenzelm
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-09-02, by wenzelm
tuned ML message;
2009-09-02, by wenzelm
added "using" to blacklist
2009-09-02, by nipkow
merged
2009-09-02, by wenzelm
merged
2009-09-02, by wenzelm
removed old Isar document model;
2009-09-01, by wenzelm
corrected spelling
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
added -q switch for run in qnd mode
2009-09-01, by haftmann
code generator is now a separate component
2009-09-01, by haftmann
tuned document
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
tuned
2009-09-01, by haftmann
avoid long line
2009-08-24, by haftmann
added txt to blacklist
2009-09-01, by nipkow
Isabelle_Process: receiver as Actor, not EventBus;
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: actions are responsible for their log messages, output is better readable
2009-09-01, by boehmes
merged
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: added preliminary documentation,
2009-09-01, by boehmes
Mirabelle: explicit command blacklist, preliminary documentation
2009-08-31, by boehmes
modernized Isar_Document;
2009-09-01, by wenzelm
modernized Thy_Header;
2009-09-01, by wenzelm
misc cleanup and internal reorganization;
2009-09-01, by wenzelm
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
2009-09-01, by wenzelm
moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-31, by krauss
moved wfrec to Recdef.thy
2009-08-31, by krauss
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
2009-08-31, by krauss
Mirabelle: handle possible parser exceptions, emit suitable log message
2009-08-31, by boehmes
merged
2009-08-31, by boehmes
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
2009-08-31, by boehmes
merged
2009-08-31, by nipkow
tuned the simp rules for Int involving insert and intervals.
2009-08-31, by nipkow
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
2009-08-31, by boehmes
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
2009-08-31, by boehmes
merged
2009-08-29, by boehmes
apply metis with found theorems in case sledgehammer was successful
2009-08-29, by boehmes
propagate theorem names, in addition to generated return message
2009-08-29, by boehmes
misc tuning;
2009-08-29, by wenzelm
eliminated hard tabs;
2009-08-29, by wenzelm
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
2009-08-29, by wenzelm
merged
2009-08-28, by wenzelm
fixed HOLogic.stringT
2009-08-28, by krauss
merged
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-08-28, by nipkow
New option ForceSystem that makes sure we *really* get the system we ask for
2009-08-28, by nipkow
selectable prover for sledgehammer, proper environment lookup
2009-08-28, by boehmes
discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28, by wenzelm
modernized messages -- eliminated ctyp/cterm operations;
2009-08-28, by wenzelm
removed spurious invocations of atp_minimize;
2009-08-28, by wenzelm
removed obsolete print_ctyp, print_cterm;
2009-08-28, by wenzelm
modernized messages -- eliminated old Display.print_cterm;
2009-08-28, by wenzelm
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
2009-08-28, by wenzelm
misc updates and tuning;
2009-08-28, by wenzelm
PDF_VIEWER: more Unix-ish behaviour on Mac OS;
2009-08-28, by wenzelm
merged
2009-08-27, by nipkow
New example: IMP
2009-08-27, by nipkow
merged
2009-08-27, by nipkow
code generator: quantifiers over {_.._::int} and {_..<_::nat}
2009-08-27, by nipkow
more stats;
2009-08-27, by wenzelm
tuned tracing;
2009-08-27, by wenzelm
merged
2009-08-27, by wenzelm
avoid macbroy21 for now -- hardware problems;
2009-08-27, by wenzelm
tuned code generation for lists
2009-08-27, by nipkow
merged
2009-08-26, by nipkow
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-08-26, by nipkow
merged
2009-08-26, by chaieb
merged
2009-08-26, by chaieb
removed unused theorem finite_Atleast_Atmost
2009-08-26, by chaieb
merged
2009-05-19, by chaieb
Derivative of general reverses
2009-05-19, by chaieb
merged
2009-08-26, by nipkow
new interval lemma
2009-08-26, by nipkow
merged
2009-08-26, by paulson
Simplified some proofs using metis.
2009-08-26, by paulson
merged
2009-08-21, by paulson
sledgehammer used to streamline protocol proofs
2009-08-14, by paulson
Put back characters that had been erased by Emacs
2009-08-14, by paulson
added further conversions and conversionals
2009-08-26, by boehmes
merged
2009-08-26, by nipkow
new lemmas
2009-08-26, by nipkow
some examples for giving measures manually
2009-08-24, by krauss
stricter condition for (binary) integer relation
2009-08-24, by boehmes
more quoting for shell variables, canonical isabelle process
2009-08-24, by boehmes
keep the modified (tested) theory,
2009-08-24, by boehmes
do not introduce additional newlines
2009-08-24, by boehmes
tuned;
2009-08-22, by wenzelm
generalized settings;
2009-08-22, by wenzelm
removed jedit setup -- now a self-contained component (external);
2009-08-22, by wenzelm
less ambitious array operations -- for improved compatibility with older versions of bash;
2009-08-22, by wenzelm
function splitarray: splightly more abstract version that accomodates older bashes;
2009-08-22, by wenzelm
fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
2009-08-21, by krauss
added Mirabelle to NEWS
2009-08-21, by boehmes
merged
2009-08-21, by boehmes
disabled refute action (needs changes in the code of refute)
2009-08-21, by boehmes
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
Mirabelle tool script conforming to standard Isabelle tool interface,
2009-08-21, by boehmes
made Mirabelle a component
2009-08-17, by boehmes
A few Isar scripts
2009-08-20, by paulson
additional checkpoints avoid problems in error situations
2009-08-15, by haftmann
tuned
2009-08-15, by haftmann
removed atp_minimize invocation
2009-08-14, by krauss
reverted accidential corruption of superscripts introduced in a508148f7c25
2009-08-14, by krauss
merged
2009-08-14, by haftmann
inserted space into message
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
corrected Pair to Char
2009-08-14, by haftmann
merged
2009-08-14, by webertj
Fixed a bug where the simplifier would hang on
2009-08-14, by webertj
merged
2009-08-13, by paulson
Removal of redundant settings of unification trace and search bounds.
2009-08-13, by paulson
Demonstrations of sledgehammer in protocol proofs.
2009-08-13, by paulson
added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-08-12, by wenzelm
merged
2009-08-11, by wenzelm
SOS: function to set default prover; output channel changed
2009-08-10, by Philipp Meyer
interrupt handler for neos csdp client
2009-08-10, by Philipp Meyer
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
2009-08-11, by wenzelm
updated generated document
2009-08-11, by haftmann
dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML
2009-08-11, by haftmann
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
2009-08-11, by haftmann
merged
2009-08-11, by haftmann
temporary adjustment to dubious state of eta expansion in recfun_codegen
2009-08-11, by haftmann
properly merged
2009-08-10, by haftmann
same_typscheme replaces ugly common_typ_eqns
2009-08-10, by haftmann
moved all technical processing of code equations to code_thingol.ML
2009-08-10, by haftmann
added map_transpose
2009-08-10, by haftmann
merged
2009-08-10, by haftmann
attempt to move desymbolization to translation
2009-08-10, by haftmann
added a somehow clueless comment
2009-07-31, by haftmann