isabelle: Graph

clarify types of terms: use proper set type
2011-10-25, by boehmes
instance bool :: linorder
2011-10-24, by huffman
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
2011-10-24, by bulwahn
fixed typo
2011-10-24, by bulwahn
latex output not needed because errors manifest themselves earlier
2011-10-24, by nipkow
some text on inner-syntax;
2011-10-23, by wenzelm
renamed in ASM
2011-10-23, by nipkow
tuned order of eqns
2011-10-23, by nipkow
tuned
2011-10-23, by nipkow
script for exporting filtered IMP files as tar.gz
2011-10-23, by kleing
removed Norbert's email from isatest (bounces)
2011-10-23, by kleing
class Lexicon as abstract datatype;
2011-10-22, by wenzelm
more private stuff;
2011-10-22, by wenzelm
class Text.Edit as abstract datatype;
2011-10-22, by wenzelm
class Time as abstract datatype;
2011-10-22, by wenzelm
class Volatile as abstract datatype;
2011-10-22, by wenzelm
merged
2011-10-22, by nipkow
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
2011-10-22, by nipkow
experimental support for Scala 2.9.1.final;
2011-10-22, by wenzelm
class Path as abstract datatype;
2011-10-22, by wenzelm
class Counter as abstract datatype;
2011-10-22, by wenzelm
discontinued redundant ASCII syntax;
2011-10-22, by wenzelm
modernized specifications;
2011-10-22, by wenzelm
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
2011-10-21, by wenzelm
merged
2011-10-21, by nipkow
tuned
2011-10-21, by nipkow
merged
2011-10-21, by wenzelm
replacing metis proofs with facts xt1 by new proof with more readable names
2011-10-21, by bulwahn
more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
2011-10-21, by blanchet
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
2011-10-21, by blanchet
NEWS
2011-10-21, by bulwahn
updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post
2011-10-21, by bulwahn
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-10-21, by bulwahn
removing redundant attribute code_inline in the code generator
2011-10-21, by bulwahn
tuned;
2011-10-21, by wenzelm
tuned;
2011-10-21, by wenzelm
improving mutabelle script again after missing some changes in f4896c792316
2011-10-21, by bulwahn
correcting code_prolog
2011-10-21, by bulwahn
merged
2011-10-21, by huffman
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
2011-10-21, by huffman
merged
2011-10-21, by nipkow
tuned
2011-10-21, by nipkow
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
2011-10-20, by blanchet
merged
2011-10-20, by huffman
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
2011-10-20, by huffman
removed [trans] concept from basic material
2011-10-20, by kleing
merged
2011-10-20, by nipkow
tuned
2011-10-20, by nipkow
merged
2011-10-20, by bulwahn
modernizing predicate_compile_quickcheck
2011-10-20, by bulwahn
adding depth as an quickcheck configuration
2011-10-20, by bulwahn
renamed name -> vname
2011-10-20, by nipkow
removed some remaining artefacts of ancient SML code generator
2011-10-19, by haftmann
NEWS
2011-10-19, by haftmann
cleaner LEO-II extensionality step detection
2011-10-19, by blanchet
marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
2011-10-19, by blanchet
one more LEO-II failure
2011-10-19, by blanchet
merged
2011-10-19, by wenzelm
merged
2011-10-19, by huffman
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
2011-10-18, by huffman
more uniform SZS status handling
2011-10-19, by blanchet
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
2011-10-19, by blanchet
merged
2011-10-19, by nipkow
renamed B to Bc
2011-10-19, by nipkow
tuned comment;
2011-10-19, by wenzelm
proper source positions for @{lemma};
2011-10-19, by wenzelm
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
2011-10-19, by wenzelm
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19, by wenzelm
tuned legacy signature;
2011-10-19, by wenzelm
further cleanup of stats (cf. 97e81a8aa277);
2011-10-19, by wenzelm
updated keywords;
2011-10-19, by wenzelm
really document just one code generator;
2011-10-19, by wenzelm
NEWS
2011-10-19, by bulwahn
removing old code generator
2011-10-19, by bulwahn
removing declaration of code_unfold to address the old code generator
2011-10-19, by bulwahn
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
2011-10-19, by bulwahn
removing documentation about the old code generator
2011-10-19, by bulwahn
removing old code generator setup for executable sets
2011-10-19, by bulwahn
removing old code generator setup for efficient natural numbers; cleaned typo
2011-10-19, by bulwahn
removing old code generator setup for real numbers; tuned
2011-10-19, by bulwahn
removing old code generator setup for rational numbers; tuned
2011-10-19, by bulwahn
removing old code generator setup for strings
2011-10-19, by bulwahn
removing old code generator setup for lists
2011-10-19, by bulwahn
removing old code generator setup for integers
2011-10-19, by bulwahn
removing old code generator for inductive predicates
2011-10-19, by bulwahn
removing quickcheck tester SML-inductive based on the old code generator
2011-10-19, by bulwahn
removing old code generator setup for inductive sets in the inductive set package
2011-10-19, by bulwahn
removing old code generator setup of inductive predicates
2011-10-19, by bulwahn
removing old code generator setup for product types
2011-10-19, by bulwahn
removing old code generator setup for function types
2011-10-19, by bulwahn
removing old code generator setup for datatypes
2011-10-19, by bulwahn
removing old code generator for recursive functions
2011-10-19, by bulwahn
removing old code generator setup in the HOL theory
2011-10-19, by bulwahn
removing invocations of the evaluation method based on the old code generator
2011-10-19, by bulwahn
removing invocations of the old code generator
2011-10-19, by bulwahn
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
2011-10-18, by blanchet
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
2011-10-18, by blanchet
tuned
2011-10-18, by bulwahn
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
2011-10-18, by bulwahn
mira: collect size of heap images
2011-10-18, by krauss
updated doc related to Satallax
2011-10-17, by blanchet
parse Satallax unsat cores
2011-10-17, by blanchet
merged
2011-10-17, by wenzelm
(old) NEWS
2011-10-17, by noschinl
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
2011-10-17, by bulwahn
always use sockets on Windows/Cygwin;
2011-10-17, by wenzelm
mira configuration: use official polyml 5.4.1 on lxbroy10
2011-10-16, by krauss
added Term.dummy_pattern conveniences;
2011-10-16, by wenzelm
slightly more standard-conformant XML parsing (see also 94033767ef9b);
2011-10-16, by wenzelm
tuned proof
2011-10-16, by haftmann
tuned type annnotation
2011-10-16, by haftmann
hide not_member as also member
2011-10-16, by haftmann
misc tuning and modernization;
2011-10-15, by wenzelm
updated to Scala 2.8.2.final;
2011-10-15, by wenzelm
prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;
2011-10-15, by wenzelm
updated to polyml-5.4.1;
2011-10-15, by wenzelm
updated to polyml-5.4.1;
2011-10-15, by wenzelm
merged
2011-10-15, by haftmann
monadic bind
2011-10-14, by haftmann
moved sublists to More_List.thy
2011-10-14, by haftmann
NEWS
2011-10-14, by haftmann
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
2011-10-14, by wenzelm
avoid very specific code equation for card; corrected spelling
2011-10-13, by haftmann
bouned transitive closure
2011-10-13, by haftmann
moved acyclic predicate up in hierarchy
2011-10-13, by haftmann
tuned
2011-10-13, by haftmann
modernized definitions
2011-10-13, by haftmann
static dummy_task (again) to avoid a few extra allocations;
2011-10-13, by wenzelm
tuned markup
2011-10-13, by noschinl
discontinued obsolete 'types' command;
2011-10-13, by wenzelm
modernized structure Induct_Tacs;
2011-10-12, by wenzelm
tuned signature;
2011-10-12, by wenzelm
misc tuning and clarification;
2011-10-12, by wenzelm
tuned ML style;
2011-10-12, by wenzelm
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-10-12, by wenzelm
discontinued obsolete alias structure ProofContext;
2011-10-12, by wenzelm
separated monotonicity reasoning and defined narrowing with while_option
2011-10-12, by nipkow
include no-smlnj targets into library (cf. e54a985daa61);
2011-10-10, by wenzelm
increasing values_timeout to avoid SML_makeall failures on our current tests
2011-10-10, by bulwahn
merged
2011-10-10, by wenzelm
removed obsolete RC tags;
2011-10-10, by wenzelm
Int.thy: discontinued some legacy theorems
2011-10-09, by huffman
Set.thy: remove redundant [simp] declarations
2011-10-09, by huffman
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
2011-10-03, by bulwahn
tune text for document generation
2011-10-03, by bulwahn
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
2011-10-03, by bulwahn
adding code equations for cardinality and (reflexive) transitive closure on finite types
2011-10-03, by bulwahn
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
2011-10-03, by bulwahn
adding lemma to List library for executable equation of the (refl) transitive closure
2011-10-03, by bulwahn
fixed typos in IMP
2011-09-29, by Jean Pichon
added nice interval syntax
2011-09-28, by nipkow
Added dependecies
2011-09-28, by nipkow
Added Hoare-like Abstract Interpretation
2011-09-28, by nipkow
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
2011-09-28, by nipkow
back to post-release mode;
2011-09-26, by wenzelm
Added tag Isabelle2011-1 for changeset 76fef3e57004
2011-10-09, by wenzelm
tuned; Isabelle2011-1
2011-10-09, by wenzelm
updated ISABELLE_HOME_USER;
2011-10-09, by wenzelm
more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;
2011-10-04, by wenzelm
Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb
2011-10-03, by wenzelm
some amendments due to Jean Pichon;
2011-10-03, by wenzelm
correct coercion generation in case of unknown map functions
2011-09-29, by traytel
proper platform_file_url for Windows UNC paths (server shares);
2011-09-28, by wenzelm
proper platform_file_url;
2011-09-27, by wenzelm
observe base URL of rendered document;
2011-09-27, by wenzelm
more README;
2011-09-27, by wenzelm
tuned README.html;
2011-09-27, by wenzelm
tuned;
2011-09-27, by wenzelm
retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
2011-09-27, by wenzelm
tuned message, which is displayed after termination of Isabelle.app on Mac OS;
2011-09-27, by wenzelm
keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";
2011-09-26, by wenzelm
tuned;
2011-09-26, by wenzelm
ensure Isabelle env;
2011-09-26, by wenzelm
Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147
2011-09-26, by wenzelm
tuned;
2011-09-26, by wenzelm
misc tuning for release;
2011-09-26, by wenzelm
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
2011-09-26, by wenzelm
makedist for release;
2011-09-26, by wenzelm
put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
2011-09-26, by blanchet
require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0
2011-09-26, by blanchet
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
2011-09-26, by blanchet
adding an example with inductive predicates to quickcheck narrowing examples
2011-09-26, by bulwahn
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
2011-09-26, by bulwahn
clarify platforms
2011-09-25, by blanchet
killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
2011-09-25, by blanchet
updated Nitpick SAT Solver doc
2011-09-25, by blanchet
update list of SAT solvers reflecting Kodkod 1.5
2011-09-25, by blanchet
tuned signature;
2011-09-25, by wenzelm
more uniform defaults;
2011-09-25, by wenzelm
Quotient_Set.thy is part of library
2011-09-25, by haftmann
fixed typo
2011-09-25, by nipkow
standardize drive letters -- important for proper document node identification;
2011-09-24, by wenzelm