isabelle: Graph

merged
2010-05-20, by bulwahn
deactivated timing of infering modes
2010-05-20, by bulwahn
adapting examples
2010-05-19, by bulwahn
changing operations for accessing data to work with contexts
2010-05-19, by bulwahn
removed unnecessary Thm.transfer in the predicate compiler
2010-05-19, by bulwahn
changing compilation to work only with contexts; adapting quickcheck
2010-05-19, by bulwahn
removing unused argument in print_modes function
2010-05-19, by bulwahn
moving towards working with proof contexts in the predicate compiler
2010-05-19, by bulwahn
improved values command to handle a special case with tuples and polymorphic predicates more correctly
2010-05-19, by bulwahn
improved behaviour of defined_functions in the predicate compiler
2010-05-19, by bulwahn
move some example files into new HOLCF/Tutorial directory
2010-05-19, by huffman
remove redundant hdvd relation
2010-05-19, by huffman
remove unnecessary constant Fixrec.bind
2010-05-19, by huffman
add section about fixrec definitions with looping simp rules
2010-05-19, by huffman
more informative error message for fixrec when continuity proof fails
2010-05-19, by huffman
determine margin just before rendering -- proper reformatting when updating;
2010-05-20, by wenzelm
simplified alignment via FlowPanel;
2010-05-20, by wenzelm
more systematic treatment of physical document wrt. font size etc.;
2010-05-20, by wenzelm
tuned;
2010-05-20, by wenzelm
general Isabelle_System.try_read;
2010-05-20, by wenzelm
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-20, by wenzelm
inverted "Freeze" to "Follow", which is the default;
2010-05-20, by wenzelm
basic controls to freeze/update prover results;
2010-05-19, by wenzelm
show fully detailed protocol messages;
2010-05-19, by wenzelm
some updates following src/Tools/jEdit/dist-template/settings;
2010-05-19, by wenzelm
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-19, by haftmann
merged
2010-05-19, by haftmann
dropped legacy_unconstrainT
2010-05-19, by haftmann
new version of triv_of_class machinery without legacy_unconstrain
2010-05-19, by haftmann
merge
2010-05-19, by haftmann
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
2010-05-19, by haftmann
remove several redundant lemmas about floor and ceiling
2010-05-18, by huffman
merged
2010-05-18, by huffman
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2010-05-17, by huffman
prefer structure Keyword and Parse;
2010-05-18, by wenzelm
merged
2010-05-18, by wenzelm
merged
2010-05-17, by huffman
remove simp attribute from square_eq_1_iff
2010-05-17, by huffman
merged
2010-05-17, by blanchet
make sure chained facts don't pop up in the metis proof
2010-05-17, by blanchet
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-17, by blanchet
generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-17, by blanchet
identify common SPASS error more clearly
2010-05-17, by blanchet
remove simp attribute from power2_eq_1_iff
2010-05-17, by huffman
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
do not open Legacy by default;
2010-05-18, by wenzelm
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-17, by wenzelm
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-17, by wenzelm
tuned;
2010-05-17, by wenzelm
tuned signature;
2010-05-17, by wenzelm
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-17, by wenzelm
centralized legacy aliases;
2010-05-17, by wenzelm
prefer structure Parse_Spec;
2010-05-16, by wenzelm
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure ValueParse to Parse_Value;
2010-05-15, by wenzelm
refer directly to structure Keyword and Parse;
2010-05-15, by wenzelm
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-05-15, by wenzelm
renamed Outer_Parse to Parse (in Scala);
2010-05-15, by wenzelm
renamed Outer_Keyword to Keyword (in Scala);
2010-05-15, by wenzelm
avoid open Conv;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
tuned;
2010-05-15, by wenzelm
merged
2010-05-15, by wenzelm
add real_le_linear to list of legacy theorem names
2010-05-15, by huffman
make SML/NJ happy
2010-05-15, by blanchet
removed unused conversions;
2010-05-15, by wenzelm
tuned header;
2010-05-15, by wenzelm
moved normarith.ML where it is actually used;
2010-05-15, by wenzelm
incorporated further conversions and conversionals, after some minor tuning;
2010-05-15, by wenzelm
eliminated redundant runtime checks;
2010-05-15, by wenzelm
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-15, by krauss
more precise dependencies for HOL-Word-SMT_Examples;
2010-05-15, by wenzelm
merged
2010-05-15, by wenzelm
merge
2010-05-14, by blanchet
added Sledgehammer documentation to TOC
2010-05-14, by blanchet
added some Sledgehammer news
2010-05-14, by blanchet
document Nitpick changes
2010-05-14, by blanchet
merge
2010-05-14, by blanchet
added Sledgehammer manual;
2010-05-14, by blanchet
renamed Sledgehammer options
2010-05-14, by blanchet
renamed options
2010-05-14, by blanchet
remove support for crashing beta solver HaifaSat
2010-05-14, by blanchet
renamed two Sledgehammer options
2010-05-14, by blanchet
merged
2010-05-14, by nipkow
added listsum lemmas
2010-05-14, by nipkow
Revert mixin patch due to inacceptable performance drop.
2010-05-14, by ballarin
add "no_atp"s to Nitpick lemmas
2010-05-14, by blanchet
query _HOME environment variables at run-time, not at build-time
2010-05-14, by blanchet
move Refute dependency from Plain to Main
2010-05-14, by blanchet
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
2010-05-14, by blanchet
recognize new Kodkod error message syntax
2010-05-14, by blanchet
improve precision of set constructs in Nitpick
2010-05-14, by blanchet
produce more potential counterexamples for subset operator (cf. quantifiers)
2010-05-14, by blanchet
improved Sledgehammer proofs
2010-05-14, by blanchet
pass "full_type" argument to proof reconstruction
2010-05-14, by blanchet
made Sledgehammer's full-typed proof reconstruction work for the first time;
2010-05-14, by blanchet
delect installed ATPs dynamically, _not_ at image built time
2010-05-14, by blanchet
Fix syntax; apparently constant apply was introduced in an earlier changeset.
2010-05-13, by ballarin
Merged.
2010-05-13, by ballarin
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-13, by ballarin
Remove improper use of mixin in class package.
2010-05-13, by ballarin
Multiset: renamed, added and tuned lemmas;
2010-05-13, by nipkow
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
2010-05-12, by huffman
more precise dependencies
2010-05-13, by boehmes
updated SMT certificates
2010-05-12, by boehmes
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12, by boehmes
integrated SMT into the HOL image
2010-05-12, by boehmes
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
2010-05-12, by boehmes
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
2010-05-12, by boehmes
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
2010-05-12, by boehmes
added tracing of reconstruction data
2010-05-12, by boehmes
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
2010-05-12, by boehmes
deleted SMT translation files (to be replaced by a simplified version)
2010-05-12, by boehmes
move the addition of extra facts into a separate module
2010-05-12, by boehmes
normalize numerals: also rewrite Numeral0 into 0
2010-05-12, by boehmes
added missing rewrite rules for natural min and max
2010-05-12, by boehmes
rewrite bool case expressions as if expression
2010-05-12, by boehmes
simplified normalize_rule and moved it further down in the code
2010-05-12, by boehmes
merged addition of rules into one function
2010-05-12, by boehmes
added simplification for distinctness of small lists
2010-05-12, by boehmes
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
2010-05-12, by boehmes
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-14, by wenzelm
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13, by wenzelm
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-13, by wenzelm
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13, by wenzelm
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13, by wenzelm
unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13, by wenzelm
added Proofterm.get_name variants according to krauss/schropp;
2010-05-13, by wenzelm
conditional structure SingleAssignment;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
tuned proofs and fact and class names
2010-05-12, by haftmann
tuned fact collection names and some proofs
2010-05-12, by haftmann
grouped local statements
2010-05-12, by haftmann
tuned test problems
2010-05-12, by haftmann
merged
2010-05-12, by wenzelm
merged
2010-05-12, by nipkow
simplified proof
2010-05-12, by nipkow
modernized specifications;
2010-05-12, by wenzelm
updated/unified some legacy warnings;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
do not emit legacy_feature warnings here -- users have no chance to disable them;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
removed some obsolete admin stuff;
2010-05-12, by wenzelm
check NEWS;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
updated some version numbers;
2010-05-12, by wenzelm
minor tuning;
2010-05-12, by wenzelm
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
modernized specifications; tuned reification
2010-05-12, by haftmann
merged
2010-05-12, by haftmann
added lemmas concerning last, butlast, insort
2010-05-12, by haftmann
Remove RANGE_WARN
2010-05-12, by Cezary Kaliszyk
clarified NEWS entry
2010-05-12, by hoelzl
merged
2010-05-12, by hoelzl
added NEWS entry
2010-05-12, by hoelzl
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
2010-05-11, by hoelzl
Add rules directly to the corresponding class locales instead.
2010-05-11, by hoelzl
Removed usage of normalizating locales.
2010-05-11, by hoelzl
speed up some proofs, fixing linarith_split_limit warnings
2010-05-11, by huffman
fix some linarith_split_limit warnings
2010-05-11, by huffman
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
2010-05-11, by huffman
fix duplicate simp rule warning
2010-05-11, by huffman
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-11, by huffman
merged
2010-05-11, by huffman
simplify code for emptiness check
2010-05-11, by huffman
removed lemma real_sq_order; use power2_le_imp_le instead
2010-05-11, by huffman
merged
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
represent de-Bruin indices simply by position in list
2010-05-11, by haftmann
tuned reification functions
2010-05-11, by haftmann
tuned code; toward a tightended interface with generated code
2010-05-11, by haftmann
fix spelling of 'superseded'
2010-05-11, by huffman
NEWS: removed theory PReal
2010-05-11, by huffman
collected NEWS updates for HOLCF
2010-05-11, by huffman
merged
2010-05-11, by huffman
move floor lemmas from RealPow.thy to RComplete.thy
2010-05-11, by huffman
add lemma tendsto_Complex
2010-05-11, by huffman
move some theorems from RealPow.thy to Transcendental.thy
2010-05-11, by huffman
add lemma power2_eq_1_iff; generalize some other lemmas
2010-05-11, by huffman
minimize imports
2010-05-10, by huffman
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
2010-05-10, by huffman
clarified Pretty.font_metrics;
2010-05-12, by wenzelm
format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
more precise pretty printing based on actual font metrics;
2010-05-11, by wenzelm
predefined spaces;
2010-05-11, by wenzelm
merged
2010-05-11, by wenzelm
support Isabelle plugin properties with defaults;
2010-05-11, by wenzelm
merged
2010-05-11, by Christian Urban
tuned proof so that no simplifier warning is printed
2010-05-11, by Christian Urban
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
tuned
2010-05-11, by haftmann
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-05-11, by haftmann
tuned; dropped strange myassoc2
2010-05-10, by haftmann
stylized COOPER exception
2010-05-10, by haftmann
simplified oracle
2010-05-10, by haftmann
shorten names
2010-05-10, by haftmann
updated references to ML files
2010-05-10, by haftmann
only one module fpr presburger method
2010-05-10, by haftmann
moved int induction lemma to theory Int as int_bidirectional_induct
2010-05-10, by haftmann
tuned theory text; dropped unused lemma
2010-05-10, by haftmann
one structure is better than three
2010-05-10, by haftmann
less complex organization of cooper source code
2010-05-10, by haftmann
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
2010-05-10, by haftmann
add real_mult_commute to legacy theorem names
2010-05-10, by huffman
new construction of real numbers using Cauchy sequences
2010-05-10, by huffman
add more credits to ex/Dedekind_Real.thy
2010-05-10, by huffman
put construction of reals using Dedekind cuts in HOL/ex
2010-05-10, by huffman
disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
2010-05-11, by wenzelm
simple dialogs: ensure Swing thread;
2010-05-10, by wenzelm
font size re-adjustment according to Lobo internals;
2010-05-10, by wenzelm
Scala for Netbeans 6.8v1.1.0rc2;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-05-10, by wenzelm
more convenient look-and-feel setup;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;
2010-05-10, by wenzelm
updated to jedit 4.3.2;
2010-05-10, by wenzelm
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-10, by wenzelm
adapted to scala-2.8.0.RC2;
2010-05-10, by wenzelm
merged
2010-05-10, by wenzelm
real_mult_commute -> mult_commute
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
remove a couple of redundant lemmas; simplify some proofs
2010-05-09, by huffman
merged
2010-05-09, by huffman
add lemmas one_less_inverse and one_le_inverse
2010-05-08, by huffman
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
2010-05-09, by krauss
added lemmas rel_comp_UNION_distrib(2)
2010-05-09, by krauss
made SML/NJ happy;
2010-05-08, by wenzelm