isabelle: Graph

multiset operations are defined with lift_definitions;
2012-04-12, by bulwahn
remove outdated comment
2012-04-12, by huffman
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-04-11, by wenzelm
standardized ML aliases;
2012-04-11, by wenzelm
clarified proof_result: finish proof formally via head tr, not end_tr;
2012-04-11, by wenzelm
tuned;
2012-04-11, by wenzelm
more robust Future.fulfill wrt. duplicate assignment and interrupt;
2012-04-11, by wenzelm
tuned message;
2012-04-11, by wenzelm
always signal after cancel_group: passive tasks may have become active;
2012-04-11, by wenzelm
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
2012-04-11, by wenzelm
merged
2012-04-10, by wenzelm
moved lift_raw_const wrapper out of the Quotient-package into Nominal2
2012-04-10, by Christian Urban
misc tuning and simplification;
2012-04-10, by wenzelm
static relevance of proof via syntax keywords;
2012-04-10, by wenzelm
tuned future priorities: print 0, goal ~1, execute ~2;
2012-04-10, by wenzelm
updated for Poly/ML SVN 1476;
2012-04-10, by wenzelm
some coverage of HOL/TPTP;
2012-04-10, by wenzelm
added graph-conversion utility for TPTP files
2012-04-10, by sultana
moved non-interpret-specific code to different module
2012-04-10, by sultana
disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
2012-04-09, by wenzelm
tuned proofs;
2012-04-09, by wenzelm
slightly faster default compilation of Isabelle/Scala;
2012-04-09, by wenzelm
more explicit last exec result;
2012-04-09, by wenzelm
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
2012-04-09, by wenzelm
tuned;
2012-04-09, by wenzelm
simplified Future.cancel/cancel_group (again) -- running threads only;
2012-04-09, by wenzelm
added ML pretty-printing;
2012-04-09, by wenzelm
merged
2012-04-07, by wenzelm
merged
2012-04-07, by wenzelm
explicit constructor Nat leaves nat_of as conversion
2012-04-07, by haftmann
abandoned almost redundant *_foldr lemmas
2012-04-06, by haftmann
tuned
2012-04-06, by haftmann
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-04-06, by haftmann
enable parallel proofs (cf. e8552cba702d), only affects packages so far;
2012-04-07, by wenzelm
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07, by wenzelm
tuned proofs;
2012-04-07, by wenzelm
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
2012-04-07, by wenzelm
tuned imports;
2012-04-07, by wenzelm
updated header keywords;
2012-04-07, by wenzelm
init message not bad;
2012-04-07, by wenzelm
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
2012-04-07, by wenzelm
discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06, by wenzelm
remove now-unnecessary type annotations from lift_definition commands
2012-04-06, by huffman
more robust generation of quotient rules using tactics
2012-04-06, by huffman
merged
2012-04-06, by huffman
add function dest_Quotient
2012-04-06, by huffman
standardized alias;
2012-04-06, by wenzelm
fixed document;
2012-04-06, by wenzelm
merged
2012-04-06, by wenzelm
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
2012-04-06, by huffman
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
2012-04-05, by kuncar
make Quotient_Def.lift_raw_const working again
2012-04-05, by kuncar
use standard quotient lemmas to generate transfer rules
2012-04-05, by huffman
add transfer lemmas for quotients
2012-04-05, by huffman
define reflp directly, in the manner of symp and transp
2012-04-05, by huffman
set up and use lift_definition for word operations
2012-04-05, by huffman
lift_definition declares transfer_rule attribute
2012-04-05, by huffman
configure transfer method for 'a word -> int
2012-04-05, by huffman
added timestamps to logging of named thms
2012-04-05, by krauss
merged
2012-04-05, by huffman
merged
2012-04-04, by huffman
add lemmas for generating transfer rules for typedefs
2012-04-04, by huffman
tuned;
2012-04-05, by sultana
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
2012-04-04, by sultana
merge
2012-04-04, by Cezary Kaliszyk
HOL/Import more precise map types
2012-04-04, by Cezary Kaliszyk
HOL/Import typed matches against Isabelle typedef result
2012-04-04, by Cezary Kaliszyk
connect the Quotient package to the Lifting package
2012-04-04, by kuncar
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04, by kuncar
tuned;
2012-04-04, by sultana
added interpretation for formula conditional;
2012-04-04, by sultana
refactored tptp lex;
2012-04-04, by sultana
refactored tptp yacc to bring close to official spec;
2012-04-04, by sultana
transfer method generalizes over free variables in goal
2012-04-04, by huffman
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-04, by huffman
update keywords file
2012-04-04, by huffman
merged
2012-04-04, by huffman
fix typos
2012-04-04, by huffman
lift_definition command generates transfer rule
2012-04-04, by huffman
prove_quot_theorem fixes types
2012-04-04, by huffman
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
2012-04-04, by bulwahn
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
2012-04-04, by bulwahn
stop node execution at first unassigned exec;
2012-04-06, by wenzelm
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-06, by wenzelm
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
2012-04-05, by wenzelm
less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05, by wenzelm
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05, by wenzelm
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
2012-04-05, by wenzelm
Command.memo including physical interrupts (unlike Lazy.lazy);
2012-04-05, by wenzelm
tuned;
2012-04-05, by wenzelm
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04, by wenzelm
proper signature constraint;
2012-04-04, by wenzelm
tuned comments;
2012-04-04, by wenzelm
separate module for prover command execution;
2012-04-04, by wenzelm
tuned;
2012-04-04, by wenzelm
fix typo in ML structure name
2012-04-04, by huffman
removed obsolete isar-overview manual;
2012-04-04, by wenzelm
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
2012-04-04, by sultana
merged
2012-04-04, by bulwahn
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-04-04, by bulwahn
improved equality check for modes in predicate compiler
2012-04-04, by bulwahn
rename ML structure to avoid shadowing earlier name
2012-04-04, by huffman
add type annotations to make SML happy (cf. ec6187036495)
2012-04-04, by huffman
merged
2012-04-03, by huffman
new transfer proof method
2012-04-03, by huffman
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03, by huffman
prefer prog-prove, suppress isar-overview;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
formal integration of "prog-prove" manual;
2012-04-03, by wenzelm
prefer static dependencies;
2012-04-03, by wenzelm
merged
2012-04-03, by huffman
modernized obsolete old-style theory name with proper new-style underscore
2012-04-03, by huffman
removed use of CharVector in generated parser, to make SMLNJ happy
2012-04-03, by sultana
avoid duplicate PIDE markup;
2012-04-03, by wenzelm
less intrusive visibility;
2012-04-03, by wenzelm
more robust re-import wrt. non-HHF assumptions;
2012-04-03, by wenzelm
consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
2012-04-03, by wenzelm
close context elements via Expression.cert/read_declaration;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
added me to isatest email list
2012-04-03, by sultana
new package Lifting - initial commit
2012-04-03, by kuncar
add floor/ceiling lemmas suggested by René Thiemann
2012-04-03, by huffman
made sure that " is shown in tutorial text
2012-04-03, by nipkow
merged
2012-04-02, by Christian Urban
tuned proofs
2012-04-02, by Christian Urban
merged
2012-04-02, by nipkow
towards showing " in the tutorial
2012-04-02, by nipkow
tuned proof in order to avoid warning message
2012-04-02, by Christian Urban
remove unnecessary qualifiers on names
2012-04-02, by huffman
add lemma Suc_1
2012-04-02, by huffman
merged
2012-04-02, by berghofe
Require "For" keyword to be followed by at least one whitespace, to avoid that
2012-04-02, by berghofe
normalize defs (again, cf. 008b7858f3c0);
2012-04-03, by wenzelm
some context examples;
2012-04-03, by wenzelm
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
2012-04-03, by wenzelm
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
2012-04-03, by wenzelm
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
2012-04-03, by wenzelm
better drop background syntax if entity depends on parameters;
2012-04-03, by wenzelm
more uniform abbrev vs. define;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
clarified generic_const vs. close_schematic_term;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more uniform theory_abbrev with const_declaration;
2012-04-03, by wenzelm
avoid const_declaration in aux. context (cf. locale_foundation);
2012-04-03, by wenzelm
clarified background_foundation vs. theory_foundation (with const_declaration);
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more general standard_declaration;
2012-04-02, by wenzelm
better restore after close_target;
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
clarified standard_declaration vs. theory_declaration;
2012-04-02, by wenzelm
smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
tuned signature;
2012-04-02, by wenzelm
misc tuning and simplification;
2012-04-02, by wenzelm
better restore to first target, not last target;
2012-04-02, by wenzelm
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
2012-04-02, by wenzelm
more general Local_Theory.restore, allow any nesting level;
2012-04-02, by wenzelm
new tutorial
2012-04-02, by nipkow
New manual Programming and Proving in Isabelle/HOL
2012-04-02, by nipkow
add simp rules for dvd on negative numerals
2012-04-02, by huffman
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
2012-04-01, by krauss
clarified terminology; added reference to bundle component
2012-04-01, by krauss
less modest NEWS; CONTRIBUTORS
2012-04-01, by krauss
renamed import session back to Import, conforming to directory name; NEWS
2012-04-01, by krauss
more precise IsaMakefile (eg. see HOL-Algebra);
2012-04-01, by wenzelm
more keywords;
2012-04-01, by wenzelm
merged
2012-04-01, by wenzelm
merged
2012-04-01, by krauss
removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare
2012-04-01, by krauss
Modernized HOL-Import for HOL Light
2012-04-01, by Cezary Kaliszyk
merged
2012-04-01, by wenzelm
adapted Mira configuration to dd04c8173bb2.
2012-04-01, by krauss
removed Nat_Numeral.thy, moving all theorems elsewhere
2012-04-01, by huffman
less brutal return from function, to allow caller to report error;
2012-04-01, by wenzelm
more general context command with auxiliary fixes/assumes etc.;
2012-04-01, by wenzelm
more precise type annotation (cf. 6523a21076a8);
2012-04-01, by wenzelm
nothing specific about named target;
2012-04-01, by wenzelm
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
2012-04-01, by wenzelm
added Attrib.global_notes/local_notes/generic_notes convenience;
2012-04-01, by wenzelm
simplified;
2012-04-01, by wenzelm
tuned signature;
2012-04-01, by wenzelm
clarified Named_Target.target_declaration: propagate through other levels as well;
2012-04-01, by wenzelm
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
2012-04-01, by wenzelm
tuned proofs
2012-04-01, by huffman
merged
2012-03-31, by huffman
tuned proof
2012-03-31, by huffman
add lemma power_le_one
2012-03-31, by huffman
tuned;
2012-03-31, by wenzelm
tuned signature;
2012-03-31, by wenzelm
more direct Local_Defs.contract;
2012-03-31, by wenzelm
more precise Local_Defs.expand wrt. *local* prems only;
2012-03-31, by wenzelm
tuned comment;
2012-03-31, by wenzelm
more robust Scala 2.9.x interpreter invocation -- avoid separate interpreter thread and thus deadlock of Swing_Thread.now;
2012-03-30, by wenzelm
tuned;
2012-03-30, by wenzelm
dropped empty files
2012-03-30, by haftmann
dropped now obsolete Cset theories
2012-03-30, by haftmann
merged
2012-03-30, by wenzelm
tuned proofs, less guesswork;
2012-03-30, by wenzelm
merged
2012-03-30, by huffman
load Tools/numeral.ML in Num.thy
2012-03-30, by huffman
tuned proof
2012-03-30, by huffman
set up numeral reorient simproc in Num.thy
2012-03-30, by huffman
remove redundant simp rule
2012-03-30, by huffman
add simp rules for eve/odd on numerals
2012-03-30, by huffman
remove content-free theory ex/Arithmetic_Series_Complex.thy
2012-03-30, by huffman
rephrase lemmas about arithmetic series using numeral '2'
2012-03-30, by huffman
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-03-30, by huffman
replace lemmas eval_nat_numeral with a simpler reformulation
2012-03-30, by huffman
restate various simp rules for word operations using pred_numeral
2012-03-30, by huffman
new lemmas for simplifying subtraction on nat numerals
2012-03-30, by huffman
removed redundant nat-specific copies of theorems
2012-03-30, by huffman
move more theorems from Nat_Numeral.thy to Num.thy
2012-03-30, by huffman
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
2012-03-30, by wenzelm
more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);
2012-03-30, by wenzelm
more explicit isatest environment settings (from private .bashrc);
2012-03-30, by wenzelm
merged
2012-03-30, by huffman
fix search-and-replace errors
2012-03-30, by huffman
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
2012-03-30, by huffman
add constant pred_numeral k = numeral k - (1::nat);
2012-03-30, by huffman
move lemmas from Nat_Numeral.thy to Nat.thy
2012-03-30, by huffman
move lemmas from Nat_Numeral to Int.thy and Num.thy
2012-03-30, by huffman
merged
2012-03-30, by bulwahn
adding theory to prove completeness of the exhaustive generators
2012-03-30, by bulwahn
refine bindings in quickcheck_common: do not conceal and do not declare as simps
2012-03-30, by bulwahn
hiding fact not so aggressively
2012-03-30, by bulwahn
power on predicate relations
2012-03-30, by haftmann
made Mirabelle-SH's 'trivial' check optional;
2012-03-30, by sultana
merged
2012-03-29, by wenzelm
more specific notion of partiality (cf. Scala version);
2012-03-29, by wenzelm
use qualified names for rsp and rep_eq theorems in quotient_def
2012-03-29, by kuncar
announcing NEWS (cf. 446cfc760ccf)
2012-03-29, by bulwahn
remove obsolete simp rule for powers
2012-03-29, by huffman
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
2012-03-29, by huffman
remove unneeded rewrite rules for powers of numerals
2012-03-29, by huffman
remove duplicate lemma Suc_numeral
2012-03-29, by huffman
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
2012-03-29, by huffman
bootstrap Num.thy before Power.thy;
2012-03-29, by huffman
educated guess to include jdk
2012-03-29, by haftmann
improved robustness with new antiquoation by Makarius
2012-03-28, by nipkow
merged
2012-03-28, by nipkow
updates
2012-03-28, by nipkow
updated documentation files (cf. c14fda8fee38)
2012-03-28, by bulwahn
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
2012-03-28, by wenzelm
merged
2012-03-28, by wenzelm
removed references to obsolete theorems
2012-03-28, by huffman
merged
2012-03-28, by bulwahn
some tuning while reviewing the current state of the quotient_def package
2012-03-28, by bulwahn
improving spelling
2012-03-28, by bulwahn
changing more definitions to quotient_definition
2012-03-28, by bulwahn
removing now redundant impl_of theorems in DAList
2012-03-28, by bulwahn
using abstract code equations for proofs of code equations in Multiset
2012-03-28, by bulwahn
simplified statements and proofs;
2012-03-28, by wenzelm
tuned whitespace;
2012-03-28, by wenzelm
updated Sign.add_type, Name_Space.declare;
2012-03-28, by wenzelm
updated comments;
2012-03-28, by wenzelm
merged
2012-03-28, by huffman
remove unnecessary rules from the simpset
2012-03-27, by huffman
remove unused premises
2012-03-27, by huffman
remove duplicate lemmas
2012-03-27, by huffman
mark some duplicate lemmas for deletion
2012-03-27, by huffman
remove more redundant lemmas
2012-03-27, by huffman
tuned proofs
2012-03-27, by huffman
remove redundant lemmas
2012-03-27, by huffman
generalized lemma zpower_zmod
2012-03-27, by huffman
remove redundant lemma
2012-03-27, by huffman
remove redundant lemma
2012-03-27, by huffman
remove duplicate [algebra] declarations
2012-03-27, by huffman
generalize more div/mod lemmas
2012-03-27, by huffman
generalize some theorems about div/mod
2012-03-27, by huffman
updated to jedit-4.5.1;
2012-03-28, by wenzelm
merged
2012-03-27, by kuncar
note a code eqn in quotient_def
2012-03-27, by kuncar
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-27, by boehmes
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
2012-03-27, by blanchet
fixed eta-extension of higher-order quantifiers in THF output
2012-03-27, by blanchet
renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-27, by blanchet
tuning
2012-03-27, by blanchet
tuning (in particular, Symtab instead of AList)
2012-03-27, by blanchet
tweak slices, based on eval by Daniel Wand
2012-03-27, by blanchet
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
2012-03-27, by blanchet
print a hint
2012-03-27, by blanchet
avoid DL
2012-03-27, by blanchet
TFF: declare free types as types
2012-03-27, by blanchet
merged
2012-03-27, by bulwahn
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
2012-03-27, by bulwahn
remove redundant lemmas
2012-03-27, by huffman
move int::ring_div instance upward, simplify several proofs
2012-03-27, by huffman
rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
2012-03-27, by huffman
extend definition of divmod_int_rel to handle denominator=0 case
2012-03-27, by huffman
tuned proofs
2012-03-27, by huffman
shorten a proof
2012-03-27, by huffman
simplify some proofs
2012-03-27, by huffman
rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
2012-03-27, by huffman
simplify some proofs
2012-03-27, by huffman
merged
2012-03-26, by wenzelm
merged
2012-03-26, by nipkow
reverted to canonical name
2012-03-26, by nipkow
merged
2012-03-26, by wenzelm
merged
2012-03-26, by huffman
revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
2012-03-26, by huffman
merged
2012-03-26, by huffman
fix incorrect code_modulename declarations
2012-03-26, by huffman
code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
2012-03-26, by huffman
remove old-style semicolon
2012-03-26, by huffman
merged
2012-03-26, by nipkow
Functions and lemmas by Christian Sternagel
2012-03-26, by nipkow
more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
2012-03-26, by wenzelm
disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
2012-03-26, by wenzelm
tuned comment
2012-03-26, by kuncar
merged
2012-03-26, by kuncar
merged
2012-03-26, by kuncar
tuned proof - no smt call
2012-03-26, by kuncar
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
2012-03-26, by wenzelm
updated theory header syntax and related details;
2012-03-26, by wenzelm
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
2012-03-24, by wenzelm
merged
2012-03-26, by wenzelm
reintroduced broken proofs and regenerated certificates
2012-03-26, by blanchet
merged, resolving trivial conflict;
2012-03-26, by wenzelm
fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-26, by blanchet
merged fork with new numeral representation (see NEWS)
2012-03-25, by huffman
merged
2012-03-24, by kuncar
use Thm.transfer for thms stored in generic context data storage
2012-03-23, by kuncar
hide invariant constant
2012-03-23, by kuncar
explicit SMTP server (appears to be required after recent change of system configuration);
2012-03-24, by wenzelm
more isatest subscribers;
2012-03-24, by wenzelm
merged
2012-03-23, by paulson
proof tidying
2012-03-23, by paulson
updated comment
2012-01-16, by kuncar
resolve invariant constant name clash
2012-03-23, by kuncar
update etc/isar-keywords.el
2012-03-23, by kuncar
fix example files
2012-03-23, by kuncar
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
2012-03-23, by kuncar
simplified code of generation of aggregate relations
2012-03-23, by kuncar
store the relational theorem for every relator
2012-03-23, by kuncar
store the quotient theorem for every quotient
2012-03-23, by kuncar
fix Quotient_Examples
2012-03-23, by kuncar
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
2012-03-23, by kuncar
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
2012-03-23, by bulwahn
tuned;
2012-03-23, by wenzelm
merged;
2012-03-22, by wenzelm
fixed typo
2012-03-22, by haftmann
more instructive NEWS
2012-03-22, by haftmann
more structured proofs
2012-03-22, by paulson
New Message
2012-03-22, by paulson
No longer treat "title" as FDL keyword
2012-03-22, by berghofe
tuned proofs;
2012-03-22, by wenzelm
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
synchronize syntax uniformly for target stack and aux. context;
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
merged
2012-03-21, by wenzelm
removed Satallax option, now that this is the default
2012-03-21, by blanchet
doc update
2012-03-21, by blanchet
improve "remote_satallax" by exploiting unsat core
2012-03-21, by blanchet
generate weights and precedences for predicates as well
2012-03-21, by blanchet
refinements to constructibility
2012-03-21, by paulson
More structured proofs for infinite cardinalities
2012-03-21, by paulson
actually expose target context;
2012-03-21, by wenzelm
more explicit Toplevel.open_target/close_target;
2012-03-21, by wenzelm
tuned signature;
2012-03-21, by wenzelm
optional 'includes' element for long theorem statements;
2012-03-21, by wenzelm
basic support for nested contexts including bundles;
2012-03-21, by wenzelm
tuned messages;
2012-03-21, by wenzelm
basic support for nested local theory targets;
2012-03-21, by wenzelm
try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;
2012-03-21, by wenzelm
improved isatest arguments for macbroy2;
2012-03-21, by wenzelm
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
2012-03-21, by wenzelm
prefer explicitly qualified exception List.Empty;
2012-03-21, by wenzelm
merged
2012-03-20, by wenzelm
refined init_model: allow change of buffer name as caused by "Save as", for example;
2012-03-20, by wenzelm
basic support for bundled declarations;
2012-03-20, by wenzelm
doc update
2012-03-20, by blanchet
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
2012-03-20, by blanchet
removed obsolete temporary hack
2012-03-20, by blanchet
tweaks
2012-03-20, by blanchet
proof tidying
2012-03-20, by paulson
minimalistic support for remote URLs: no master dir here;
2012-03-20, by wenzelm
optimized "metis" call
2012-03-20, by blanchet
added term_order option to Mirabelle
2012-03-20, by blanchet
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
2012-03-20, by blanchet
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
2012-03-20, by blanchet
remove two options that were found to play hardly any role
2012-03-20, by blanchet
enable "metis_advisory_simp" by default
2012-03-20, by blanchet
more stats;
2012-03-20, by wenzelm
merged
2012-03-20, by paulson
more structured proofs
2012-03-20, by paulson
don't generate new SPASS constructs for old SPASS
2012-03-20, by blanchet
tune Metis example
2012-03-20, by blanchet
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-03-20, by blanchet
continued implementation of term ordering attributes
2012-03-20, by blanchet
added "dont_preplay" alias
2012-03-20, by blanchet
document "dont_preplay"
2012-03-20, by blanchet
tuning
2012-03-20, by blanchet
implement term order attribute (for experiments)
2012-03-20, by blanchet
tuning -- don't refer to old, internal version number (needlessly confusing now)
2012-03-20, by blanchet
more weight attribute tuning
2012-03-20, by blanchet
use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
2012-03-20, by blanchet
internal renamings
2012-03-20, by blanchet
renamed E weight attribute
2012-03-20, by blanchet
tuned proofs;
2012-03-19, by wenzelm
explicit propagation of assignment event, even if changed command set is empty;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
updated Misc_Legacy.freeze_thaw;
2012-03-19, by wenzelm
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
2012-03-19, by wenzelm
moved some legacy stuff;
2012-03-19, by wenzelm
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
2012-03-19, by wenzelm
merged
2012-03-19, by wenzelm
merged
2012-03-19, by paulson
More structured proofs for cardinalities
2012-03-19, by paulson
merged
2012-03-19, by paulson
more structured case and induction proofs
2012-03-16, by paulson
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
2012-03-19, by blanchet
allow keyword tags to be redefined, but not the command category;
2012-03-19, by wenzelm
further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;
2012-03-19, by wenzelm
clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-19, by wenzelm
more robust bash interpolation;
2012-03-18, by wenzelm
more ambitious scalac options for makedist;
2012-03-18, by wenzelm
less noisy Isabelle/Scala build process;
2012-03-18, by wenzelm
comment;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned structure;
2012-03-18, by wenzelm
comments for uniformity
2012-03-18, by haftmann
proper naming of simprocs according to actual target context;
2012-03-17, by wenzelm
amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
2012-03-17, by wenzelm
more precise syntax;
2012-03-17, by wenzelm
more antiquotations;
2012-03-17, by wenzelm
misc tuning to accomodate scala-2.10.0-M2;
2012-03-17, by wenzelm
include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;
2012-03-17, by wenzelm
merged
2012-03-17, by wenzelm
merged
2012-03-17, by paulson
tidying and structured proofs
2012-03-17, by paulson
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
simultaneous read_fields -- e.g. relevant for sort assignment;
2012-03-17, by wenzelm
added Syntax.read_typs;
2012-03-17, by wenzelm
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
2012-03-17, by wenzelm
tuned message;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
tuned exception;
2012-03-17, by wenzelm
merged;
2012-03-17, by wenzelm
spelt out missing colemmas
2012-03-17, by haftmann
generalized INF_INT_eq, SUP_UN_eq
2012-03-17, by haftmann
tuned specifications
2012-03-16, by haftmann
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
2012-03-17, by wenzelm
tuned grouping -- merely indicate order of magnitude;
2012-03-17, by wenzelm
slightly more parallel find_theorems;
2012-03-17, by wenzelm
'definition' no longer exports the foundational "raw_def";
2012-03-17, by wenzelm
some attempts to fit source on screen;
2012-03-17, by wenzelm
eliminated odd 'finalconsts' / Theory.add_finals;
2012-03-16, by wenzelm
modernized axiomatization;
2012-03-16, by wenzelm
modernized axiomatization;
2012-03-16, by wenzelm
afford strict Args.type_name (cf. 29e88714ffe4);
2012-03-16, by wenzelm
check declared vs. defined commands at end of session;
2012-03-16, by wenzelm
more abstract heading level;
2012-03-16, by wenzelm
less redundant data;
2012-03-16, by wenzelm
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
2012-03-16, by wenzelm
merged
2012-03-16, by wenzelm
ZF news
2012-03-16, by paulson
merged
2012-03-16, by paulson
Structured transfinite induction proofs
2012-03-16, by paulson
make more word theorems respect int/bin distinction
2012-03-16, by huffman
outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16, by wenzelm
refute_params are given in *this* theory;
2012-03-16, by wenzelm
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-16, by wenzelm
define keywords early when processing the theory header, before running the body commands;
2012-03-16, by wenzelm
clarified Keyword.is_keyword: union of minor and major;
2012-03-16, by wenzelm
Isabelle/jEdit supports user-defined Isar commands within the running session;
2012-03-15, by wenzelm
merged
2012-03-15, by wenzelm
beautification and structured proofs
2012-03-15, by paulson
replacing ":" by "\<in>"
2012-03-15, by paulson
Rewrote some induction proofs to be structured
2012-03-15, by paulson
more precise TPTP keywords and dependencies;
2012-03-15, by wenzelm
declare command keywords via theory header, including strict checking outside Pure;
2012-03-15, by wenzelm
prefer formally checked @{keyword} parser;
2012-03-15, by wenzelm
added ML antiquotation @{keyword};
2012-03-15, by wenzelm
declare minor keywords via theory header;
2012-03-15, by wenzelm
more explicit header_edits before main text_edits;
2012-03-15, by wenzelm
declare keywords as side-effect of header edit;
2012-03-15, by wenzelm
more recent recent_syntax, e.g. relevant for document rendering during startup;
2012-03-15, by wenzelm
clarified syntax of prospective keywords;
2012-03-15, by wenzelm
basic support for outer syntax keywords in theory header;
2012-03-15, by wenzelm
maintain Version.syntax within document state;
2012-03-15, by wenzelm
explicit Outer_Syntax.Decl;
2012-03-15, by wenzelm
allow multiple 'keywords' as in 'fixes';
2012-03-15, by wenzelm
some support for outer syntax keyword declarations within theory header;
2012-03-15, by wenzelm
merged
2012-03-14, by wenzelm
merged
2012-03-14, by paulson
structured case and induct rules
2012-03-14, by paulson
rudimentary documentation test
2012-03-14, by haftmann
doc-src build option (for emerging mira configuration)
2012-03-14, by haftmann
corrected fragile proof; tuned semicolons
2012-03-14, by haftmann
rudimentary distribution build configuration
2012-03-14, by haftmann
support for non-HTTP repository locations (important for mira); quasi-hardwired repository name
2012-03-14, by haftmann
corrected slip
2012-03-14, by haftmann
merged
2012-03-14, by paulson
rationalising the induction rule trans_induct3
2012-03-14, by paulson
allow modification of REPOS_NAME and REPOS from outside
2012-03-14, by haftmann
locale expressions without source positions;
2012-03-14, by wenzelm
tuned;
2012-03-14, by wenzelm
tuned messages;
2012-03-14, by wenzelm
source positions for locale and class expressions;
2012-03-14, by wenzelm
some proof indentation;
2012-03-14, by wenzelm
more explicit indication of swing thread context;
2012-03-14, by wenzelm
more indentation;
2012-03-14, by wenzelm
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
2012-03-14, by wenzelm
eliminated obsolete sanitize_name;
2012-03-14, by wenzelm
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
2012-03-14, by wenzelm
more parallel inductive_cases;
2012-03-14, by wenzelm
misc tuning;
2012-03-14, by wenzelm
updated to jedit_build-20120313 with jedit-4.5.0;
2012-03-13, by wenzelm
tuned context specifications and proofs;
2012-03-13, by wenzelm
tuned proofs;
2012-03-13, by wenzelm
clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-13, by wenzelm
more explicit indication of def names;
2012-03-13, by wenzelm
merged
2012-03-13, by paulson
Structured proofs concerning the square of an infinite cardinal
2012-03-13, by paulson
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
improved attribute "abs_def" to handle object-equality as well;
2012-03-13, by wenzelm
merged
2012-03-13, by wenzelm
More structured proofs about cardinal arithmetic
2012-03-13, by paulson
tuned proofs;
2012-03-13, by wenzelm
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-13, by wenzelm
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-03-13, by wenzelm
proper printing of empty binding (again, cf. 93f6f24010c2);
2012-03-13, by wenzelm
tuned;
2012-03-13, by wenzelm
tuned strip_alls;
2012-03-13, by wenzelm
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
2012-03-13, by wenzelm
some grouping of Par_List operations, to adjust granularity;
2012-03-12, by wenzelm
Par_List.map is already smart;
2012-03-12, by wenzelm
some support for grouped list operations;
2012-03-12, by wenzelm
merged;
2012-03-12, by wenzelm
merged
2012-03-12, by noschinl
NEWS
2012-03-12, by noschinl
use eventually_elim method
2012-03-12, by noschinl
add eventually_elim method
2012-03-12, by noschinl
merged
2012-03-12, by noschinl
tuned proofs
2012-03-12, by noschinl
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12, by noschinl
tuned simpset
2012-03-12, by noschinl
activate_notes in parallel -- to speedup main operation of locale interpretation;
2012-03-12, by wenzelm
refined activate_notes: simultaneous transformation before activation;
2012-03-12, by wenzelm
tuned headers;
2012-03-12, by wenzelm
merged
2012-03-12, by paulson
Structured proofs in ZF
2012-03-12, by paulson
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
2012-03-12, by wenzelm
updated polyml/build option to prefer included libffi;
2012-03-12, by wenzelm
tuned signature;
2012-03-12, by wenzelm
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
2012-03-12, by wenzelm
merged
2012-03-11, by wenzelm
renewing Executable_Relation
2012-03-11, by bulwahn
tuned;
2012-03-11, by wenzelm
more direct Name_Space.defined_entry;
2012-03-11, by wenzelm
eliminated old-fashioned 'constrains' element;
2012-03-11, by wenzelm
modernized locale expression, with some fluctuation of arguments;
2012-03-11, by wenzelm
simplified span class in conformance to Scala version;
2012-03-10, by wenzelm
discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
2012-03-10, by wenzelm
merged
2012-03-10, by wenzelm
adding tags to quickcheck's result
2012-03-10, by bulwahn
clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval;
2012-03-10, by wenzelm
eliminated dead code;
2012-03-10, by wenzelm
clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;
2012-03-10, by wenzelm
misc tuning and simplification;
2012-03-10, by wenzelm
tuned;
2012-03-10, by wenzelm
clarified Pattern.matchess;
2012-03-10, by wenzelm
tuned;
2012-03-10, by wenzelm
more precise alignment of begin/end, proof/qed;
2012-03-10, by wenzelm
merged
2012-03-09, by wenzelm
beautified
2012-03-09, by haftmann
more precise checking for wellformedness of mapper, before and after morphism application
2012-03-09, by haftmann
reject mapper terms with type variables not contained in the term's type
2012-03-09, by haftmann
always bracket case expressions in Scala
2012-03-09, by haftmann
tuned signature;
2012-03-09, by wenzelm
merges
2012-03-09, by paulson
More calculation-based cardinality proofs
2012-03-09, by paulson
split make_tptp_parser into two scripts, for parser and lib respectively;
2012-03-09, by sultana
added ml-yacc library sources;
2012-03-09, by sultana
added tptp parser;
2012-03-09, by sultana
merged
2012-03-08, by wenzelm
Structured and calculation-based proofs (with new trans rules!)
2012-03-08, by paulson
Structured and calculation-based proofs (with new trans rules!)
2012-03-08, by paulson
tuned comment;
2012-03-08, by wenzelm
simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2012-03-08, by wenzelm
tuned;
2012-03-08, by wenzelm
clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
2012-03-08, by wenzelm
more precise warning/error positions;
2012-03-08, by wenzelm
merged
2012-03-07, by wenzelm
less rigorous but more realistic migration recommendation; note on code generation of sets
2012-03-07, by haftmann
tuned syntax; more candidates
2012-03-07, by haftmann
tuned message (cf. ML version);
2012-03-07, by wenzelm
eliminated dead code;
2012-03-07, by wenzelm
tuned signature;
2012-03-07, by wenzelm
simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);
2012-03-07, by wenzelm
to_pred/set attributes now properly handle variables of type "... => T set"
2012-03-07, by berghofe
some recovery of IsaMakefile targets from f3c10e908f65;
2012-03-07, by wenzelm
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
2012-03-07, by sultana
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
2012-03-07, by sultana
added Mirabelle action info in its log file; tuned;
2012-03-07, by sultana
More mathematical symbols for ZF examples
2012-03-06, by paulson
mathematical symbols for Isabelle/ZF example theories
2012-03-06, by paulson
Using mathematical notation for <-> and cardinal arithmetic
2012-03-06, by paulson
mathematical symbols instead of ASCII
2012-03-06, by paulson
addressed a quotient-type-related issue that arose with the port to "set"
2012-03-04, by blanchet
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
2012-03-04, by blanchet
updates for jedit-4.5.0 (still inactive);
2012-03-04, by wenzelm
more explicit patches;
2012-03-04, by wenzelm
tuned comment;
2012-03-04, by wenzelm
removed obsolete proper_command_at (cf. 03a2dc9e0624);
2012-03-04, by wenzelm
added Command.proper_range (still unused);
2012-03-04, by wenzelm
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
2012-03-04, by wenzelm
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
2012-03-04, by wenzelm
tuned
2012-03-04, by haftmann
move test targets to test target
2012-03-04, by haftmann
dropped images for importer sessions
2012-03-04, by haftmann
dropped dead code
2012-03-04, by haftmann
more accurate dependencies
2012-03-04, by haftmann
tuned ML
2012-03-04, by haftmann
dropped silly code
2012-03-04, by haftmann
tuned
2012-03-04, by haftmann
dropped dead code
2012-03-04, by haftmann
actually add "the" Importer theory
2012-03-04, by haftmann
avoid internal hol4 name references in generic importer code
2012-03-04, by haftmann
generalized user-visible text
2012-03-03, by haftmann
generalized attribute name
2012-03-03, by haftmann
dropped dead theories
2012-03-03, by haftmann
one unified Importer theory
2012-03-03, by haftmann
added actual dependencies
2012-03-03, by haftmann
import all importer theories in compatibility layer
2012-03-03, by haftmann
merged;
2012-03-03, by wenzelm
dropped obsolete ROOT.ML
2012-03-03, by haftmann
plugged in pre-existing theories appropriately
2012-03-03, by haftmann
switch of target Import-HOL_Light-Imported: not operative at the moment
2012-03-03, by haftmann
turn on quick and dirty in batch mode
2012-03-03, by haftmann
tuned whitespace
2012-03-03, by haftmann
file system structure separating HOL4 and HOL Light concerns
2012-03-03, by haftmann
distribution of compatibility theories
2012-03-03, by haftmann
formal infrastructure for import sessions
2012-03-03, by haftmann
dropped dead code
2012-03-03, by haftmann
tuned whitespace
2012-03-03, by haftmann
spurious set/pred correction
2012-03-03, by haftmann
explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction
2012-03-03, by haftmann
explicit locations for import_theory and setup_theory, for better user interface conformance
2012-03-03, by haftmann
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
canonical argument order for attribute application;
2012-03-03, by wenzelm
clarified terminology of raw protocol messages;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned signature -- emphasize Isabelle_Process Input vs. Output;
2012-03-03, by wenzelm
explicit syslog_limit reduces danger of low-level message flooding;
2012-03-03, by wenzelm
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
2012-03-03, by wenzelm
clarified scope of exception handlers;
2012-03-03, by wenzelm
relevant timing as in ML;
2012-03-03, by wenzelm
more fundamental pred-to-set conversions for range and domain by means of inductive_set
2012-03-02, by haftmann
merged
2012-03-02, by wenzelm
tuned whitespace
2012-03-02, by haftmann
tuned import
2012-03-02, by haftmann
dropped dead code
2012-03-02, by haftmann
terminate after first exception -- avoid syslog flooding;
2012-03-02, by wenzelm
avoid buffer loading overrun;
2012-03-02, by wenzelm
merged
2012-03-02, by wenzelm
collecting all axioms in a locale context in quickcheck;
2012-03-02, by bulwahn
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-03-02, by bulwahn
removing finiteness goals
2012-03-02, by bulwahn
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2012-03-02, by bulwahn
Symbol.encode header edits;
2012-03-01, by wenzelm
merged
2012-03-01, by wenzelm
tuned whitespace
2012-03-01, by haftmann
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-03-01, by haftmann
Removal of obsolete ML bindings
2012-03-01, by paulson
more robust locking;
2012-03-01, by wenzelm
proper update_header;
2012-03-01, by wenzelm
refined node_header -- more direct buffer access (again);
2012-03-01, by wenzelm
merged
2012-03-01, by wenzelm
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
2012-03-01, by blanchet
fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
2012-03-01, by blanchet
more robust set element extractor
2012-03-01, by blanchet
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
2012-03-01, by boehmes
tuned proofs;
2012-03-01, by wenzelm
more tolerant cygpath invocation, allow empty CLASSPATH;
2012-03-01, by wenzelm
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
2012-03-01, by wenzelm
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
2012-03-01, by wenzelm
more defensive node_header;
2012-02-29, by wenzelm
clarified module Thy_Load;
2012-02-29, by wenzelm
SMT fails if the chosen SMT solver is not installed
2012-02-29, by boehmes
merged
2012-02-28, by wenzelm
speed up Sledgehammer's clasimpset lookup a bit
2012-02-28, by blanchet
use SPASS instead of E for Metis examples -- it's seems faster for these small problems
2012-02-28, by blanchet
spelling
2012-02-28, by blanchet
avoid undeclared variables in let bindings;
2012-02-28, by wenzelm
tuned proofs;
2012-02-28, by wenzelm
more release tests;
2012-02-28, by wenzelm
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-28, by wenzelm
Finish localizing the quotient package.
2012-02-28, by Cezary Kaliszyk
merged
2012-02-28, by berghofe
Added infrastructure for mapping SPARK field / constructor names
2012-02-28, by berghofe
Use long prefix rather than short package name to disambiguate constant names
2012-02-27, by berghofe
more explicit development graph;
2012-02-27, by wenzelm
removed dead code (cf. a34d89ce6097);
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
removed introiff (cf. b09afce1e54f);
2012-02-27, by wenzelm
tuned;
2012-02-27, by wenzelm
removed broken/unused introiff (cf. d452117ba564);
2012-02-27, by wenzelm
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
2012-02-27, by wenzelm
tuned;
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
prefer uniform Timing.message -- avoid assumption about sequential execution;
2012-02-27, by wenzelm
prefer final ADTs -- prevent ooddities;
2012-02-27, by wenzelm
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-02-27, by wenzelm
more standard settings -- refer to COMPONENT at most once;
2012-02-27, by wenzelm
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
2012-02-27, by wenzelm
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-02-27, by wenzelm
eliminated odd comment from distant past;
2012-02-27, by wenzelm
updated cut_tac, without loose references to implementation manual;
2012-02-27, by wenzelm
updated generated file;
2012-02-27, by wenzelm
simplified cut_tac (cf. d549b5b0f344);
2012-02-27, by wenzelm
merged
2012-02-27, by huffman
avoid using constant Int.neg
2012-02-27, by huffman
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
2012-02-27, by wenzelm
merged
2012-02-27, by nipkow
added lemma
2012-02-27, by nipkow
converting "set [...]" to "{...}" in evaluation results
2012-02-27, by nipkow
removing Find_Unused_Assms_Examples from session as it requires much time
2012-02-27, by bulwahn
restored accidental omission
2012-02-26, by haftmann
dropped dead code
2012-02-26, by haftmann
tuned structure
2012-02-26, by haftmann
retain syntax here
2012-02-26, by haftmann
tuned structure; dropped already existing syntax declarations
2012-02-26, by haftmann
tuned syntax declarations; tuned structure
2012-02-26, by haftmann
merged
2012-02-26, by wenzelm
marked candidates for rule declarations
2012-02-26, by haftmann
include warning messages in node status;
2012-02-26, by wenzelm
tuned signature (in accordance with ML);
2012-02-26, by wenzelm
more PIDE modules;
2012-02-26, by wenzelm
tuned proofs;
2012-02-26, by wenzelm
more abstract class Document.State;
2012-02-26, by wenzelm
more abstract class Document.State.Assignment;
2012-02-26, by wenzelm
tuned signature;
2012-02-26, by wenzelm
more abstract class Document.Version;
2012-02-26, by wenzelm
more abstract class Document.Node;
2012-02-26, by wenzelm
more abstract class Document.History;
2012-02-26, by wenzelm
more abstract class Document.Change;
2012-02-26, by wenzelm
tuned;
2012-02-26, by wenzelm
tuned signature;
2012-02-26, by wenzelm
merged
2012-02-25, by wenzelm
slightly changing the enumeration scheme
2012-02-25, by bulwahn
adding some more test invocations of find_unused_assms
2012-02-25, by bulwahn
adding an example where random beats exhaustive testing
2012-02-25, by bulwahn
removing unnecessary assumptions in RComplete;
2012-02-25, by bulwahn
removing unnecessary assumptions in RealDef;
2012-02-25, by bulwahn
one general list_all2_update_cong instead of two special ones
2012-02-25, by bulwahn
tuned comments;
2012-02-25, by wenzelm
standard Graph instances;
2012-02-25, by wenzelm
clarified signature -- avoid oddities of Iterable like Iterator.map;
2012-02-25, by wenzelm
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
2012-02-25, by wenzelm
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
explicit is better than implicit
2012-02-24, by haftmann
dropped dead code
2012-02-24, by haftmann
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
2012-02-24, by wenzelm
tuned imports;
2012-02-24, by wenzelm
tuned signature;
2012-02-24, by wenzelm
discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);
2012-02-24, by wenzelm
merged
2012-02-24, by wenzelm
remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
2012-02-24, by huffman
avoid using Int.succ_def in proofs
2012-02-24, by huffman
avoid using Int.succ or Int.pred in proofs
2012-02-24, by huffman
avoid using BIT_simps in proofs;
2012-02-24, by huffman
avoid using BIT_simps in proofs
2012-02-24, by huffman
updated stats according to src/HOL/IsaMakefile;
2012-02-24, by wenzelm
more precise clean target;
2012-02-24, by wenzelm
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
2012-02-24, by wenzelm
avoid using Int.Pls_def in proofs
2012-02-24, by huffman
remove ill-formed lemmas word_pred_0_Min and word_m1_Min
2012-02-24, by huffman
remove ill-formed lemma of_bl_no; adapt proofs
2012-02-24, by huffman
adapt lemma mask_lem to respect int/bin distinction
2012-02-24, by huffman
rephrase some slow "metis" calls
2012-02-24, by blanchet
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24, by blanchet
general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
2012-02-24, by blanchet
renamed 'try_methods' to 'try0'
2012-02-24, by blanchet
doc fixes (thanks to Nik)
2012-02-24, by blanchet
fixed arity bug with "If" helpers for "If" that returns a function
2012-02-24, by blanchet
given up disfruitful branch
2012-02-24, by haftmann
explicit remove of lattice notation
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23, by haftmann
dropped dead code
2012-02-23, by haftmann
tuned isatest settings;
2012-02-23, by wenzelm
merged
2012-02-23, by wenzelm
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-23, by haftmann
tuned whitespace
2012-02-23, by haftmann
tuned proof
2012-02-23, by haftmann
prefer actual syntax categories;
2012-02-23, by wenzelm
avoid trait Addable, which is deprecated in scala-2.9.x;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned -- avoid copy of empty value;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype, eliminating odd representation class;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
merged
2012-02-23, by huffman
make more simp rules respect int/bin distinction
2012-02-23, by huffman
make bool list functions respect int/bin distinction
2012-02-23, by huffman
merged;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2012-02-23, by wenzelm
further graph operations from ML;
2012-02-23, by wenzelm
removed dead code;
2012-02-23, by wenzelm
directed graphs (in Scala);
2012-02-23, by wenzelm
make uses of bin_split respect int/bin distinction
2012-02-23, by huffman
remove lemma bin_cat_Pls, which doesn't respect int/bin distinction
2012-02-23, by huffman
make uses of constant bin_sc respect int/bin distinction
2012-02-23, by huffman
remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc
2012-02-23, by huffman
remove unused lemmas
2012-02-23, by huffman
simplify proofs
2012-02-23, by huffman
make uses of bin_sign respect int/bin distinction
2012-02-23, by huffman
removed unnecessary lemma zero_bintrunc
2012-02-23, by huffman
remove unnecessary lemmas
2012-02-23, by huffman
removed unnecessary constant bin_rl
2012-02-23, by huffman
remove duplication of lemmas bin_{rest,last}_BIT
2012-02-23, by huffman
remove lemmas Bit{0,1}_div2
2012-02-23, by huffman
simplify proof
2012-02-23, by huffman
deal with FIXMEs for linarith examples
2012-02-23, by huffman
CONTRIBUTORS
2012-02-23, by haftmann
merged
2012-02-22, by huffman
tuned whitespace
2012-02-22, by huffman
tuned whitespace
2012-02-22, by huffman
adding documentation about find_unused_assms command and use_subtype option in the IsarRef
2012-02-22, by bulwahn
NEWS
2012-02-22, by bulwahn
adding some examples with find_unused_assms command
2012-02-22, by bulwahn
adding new command "find_unused_assms"
2012-02-22, by bulwahn
removing some unnecessary premises from Map theory
2012-02-22, by bulwahn
preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
2012-02-22, by bulwahn
generalizing inj_on_Int
2012-02-22, by bulwahn
moving Quickcheck's example to its own session
2012-02-22, by bulwahn
tuned proofs;
2012-02-21, by wenzelm
more robust visible_range: allow empty view;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
merged;
2012-02-21, by wenzelm
made SML/NJ happy;
2012-02-21, by wenzelm
tuned proofs;
2012-02-21, by wenzelm
merged
2012-02-21, by wenzelm
tuned proofs;
2012-02-21, by wenzelm
approximate Perspective.full within the bounds of the JVM;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
invoke later to reduce chance of causing deadlock;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
separate module for text status overview;
2012-02-21, by wenzelm
overview.delay_repaint: avoid wasting GUI cycles via update_delay;
2012-02-21, by wenzelm
tuned;
2012-02-21, by wenzelm
merged
2012-02-21, by berghofe
merged
2012-02-21, by berghofe
Fixed bugs:
2012-02-20, by berghofe
merged
2012-02-21, by bulwahn
subtype preprocessing in Quickcheck;
2012-02-21, by bulwahn
adding parsing of an optional predicate with quickcheck_generator command
2012-02-21, by bulwahn
updated generated files (cf. 8d51b375e926);
2012-02-21, by wenzelm
merged;
2012-02-21, by wenzelm
add missing lemmas to compute_div_mod
2012-02-21, by huffman
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
2012-02-21, by huffman
avoid using constant Int.neg
2012-02-21, by huffman
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
2012-02-21, by huffman
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-21, by haftmann
tuned whitespace
2012-02-20, by haftmann
tuned proof
2012-02-20, by haftmann
tuned proof
2012-02-19, by haftmann
distributed lattice properties of predicates to places of instantiation
2012-02-19, by haftmann
removing some unnecessary premises from Divides
2012-02-20, by bulwahn
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
2012-02-20, by huffman
observe HEIGHT of overview ticks;
2012-02-20, by wenzelm
more careful painting of overview component: more precise and more efficient;
2012-02-20, by wenzelm
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
2012-02-20, by wenzelm
use qualified constant names instead of suffixes (from Florian Haftmann)
2012-02-20, by huffman
tuned proofs
2012-02-18, by haftmann
tuned
2012-02-12, by haftmann
brute-force adjustion
2012-02-11, by haftmann
tuned whitespace
2012-02-11, by haftmann
tuned
2012-02-11, by haftmann
tuned
2012-02-10, by haftmann
tuned code
2012-02-10, by haftmann
dropped whitespace
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
corrected typo
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
notepad is more appropriate here
2012-02-12, by haftmann
corrected treatment of applications of built-in functions to higher-order terms
2012-02-18, by boehmes
NEWS
2012-02-18, by krauss
merged
2012-02-18, by krauss
added congruence rules for Option.{map|bind}
2012-02-18, by krauss
updated generated documents
2012-02-18, by haftmann
avoid redefinition of @{theory} antiquotation
2012-02-18, by haftmann
update of generated documents
2012-02-18, by haftmann
tuned whitespace
2012-02-18, by haftmann
clarified
2012-02-18, by haftmann
corrected spelling
2012-02-18, by haftmann
clarified
2012-02-18, by haftmann
more precise semantics of "theory" antiquotation
2012-02-18, by haftmann
tuned import
2012-02-18, by haftmann
dropped references to obsolete theories
2012-02-18, by haftmann
adjusted to set type constructor
2012-02-18, by haftmann
tuned whitespace
2012-02-18, by haftmann
more explicit error on malformed abstract equation; dropped dead code; tuned signature
2012-02-18, by haftmann
simplified configuration options for syntax ambiguity;
2012-02-17, by wenzelm
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
2012-02-17, by wenzelm
more antiquotations;
2012-02-16, by wenzelm
more symbols;
2012-02-16, by wenzelm
tuned imports;
2012-02-16, by wenzelm
tuned proofs;
2012-02-16, by wenzelm
simplified configuration options for syntax ambiguity;
2012-02-16, by wenzelm
merged
2012-02-16, by wenzelm
removing unnecessary premise from diff_single_insert
2012-02-16, by bulwahn
explicit is better than implicit;
2012-02-16, by wenzelm
more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);
2012-02-16, by wenzelm
simplifying proof
2012-02-16, by bulwahn
removing unnecessary premises in theorems of List theory
2012-02-16, by bulwahn
tuning mutabelle script
2012-02-16, by bulwahn
adding documentation for abort_potential option in quickcheck
2012-02-16, by bulwahn
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-15, by wenzelm
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
2012-02-15, by wenzelm
uniform Isar source formatting for this file;
2012-02-15, by wenzelm
clarified outer syntax "constdecl", which is only local to some rail diagrams;
2012-02-15, by wenzelm
discontinued obsolete "prems" fact;
2012-02-15, by wenzelm
eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2012-02-15, by wenzelm
removed obsolete files;
2012-02-15, by wenzelm
more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);
2012-02-15, by wenzelm
removed dead code;
2012-02-15, by wenzelm
updated listrel (cf. 80dccedd6c14);
2012-02-15, by wenzelm
removed redundant cut_inst_tac -- already covered in implementation manual;
2012-02-15, by wenzelm
updated rewrite_goals_rule, rewrite_rule;
2012-02-15, by wenzelm
NEWS;
2012-02-15, by wenzelm
updated refs;
2012-02-15, by wenzelm
renamed "xstr" to "str_token";
2012-02-15, by wenzelm
merged
2012-02-14, by wenzelm
don't report spurious LEO-II errors
2012-02-14, by blanchet
better error message
2012-02-14, by blanchet
removing debug code in mutabelle
2012-02-14, by bulwahn
adding abort_potential functionality in quickcheck
2012-02-14, by bulwahn
adding abort_potential configuration in Quickcheck
2012-02-14, by bulwahn
clarified bires_inst_tac: retain internal exceptions;
2012-02-14, by wenzelm
tuned signature;
2012-02-14, by wenzelm
more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;
2012-02-14, by wenzelm
more conventional tactic setup;
2012-02-14, by wenzelm
eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
2012-02-14, by wenzelm
prefer high-level elim_format;
2012-02-14, by wenzelm
discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
2012-02-14, by wenzelm