isabelle: Graph

Cleaner implementation of sublocale command.
2010-05-24, by ballarin
Reapply mixin patch: base for performance improvements.
2010-05-24, by ballarin
merged
2010-05-23, by huffman
declare a few more cont2cont rules
2010-05-23, by huffman
HOLCF no longer redefines 'consts' command
2010-05-22, by huffman
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
2010-05-22, by huffman
simplify fixrec continuity tactic
2010-05-22, by huffman
used sledgehammer[isar_proof] to replace slow metis call
2010-05-23, by krauss
Typo fixed.
2010-05-23, by webertj
Typo fixed.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
Improved document structure.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
merged
2010-05-23, by webertj
Refactoring, minor extensions (e.g., church_rosser).
2010-05-23, by webertj
NEWS: removed fixrec_simp attribute
2010-05-22, by huffman
merged
2010-05-22, by huffman
disambiguate some syntax
2010-05-22, by huffman
optimize continuity proofs in fixrec package, using cont2cont rules
2010-05-22, by huffman
add beta_cfun simproc, which uses cont2cont rules
2010-05-22, by huffman
removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-22, by huffman
simplify definition of eta_tac
2010-05-22, by huffman
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22, by huffman
remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-22, by huffman
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-22, by huffman
merged
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
localized properties_for_sort
2010-05-22, by haftmann
@tailrec annotation;
2010-05-24, by wenzelm
renamed "rev" to "reverse" following usual Scala conventions;
2010-05-24, by wenzelm
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
2010-05-22, by wenzelm
added rev_iterator;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
access statically typed dockable windows;
2010-05-22, by wenzelm
simplified dockables using class Dockable;
2010-05-22, by wenzelm
generic dockable window;
2010-05-22, by wenzelm
separate event bus and dockable for raw output (stdout);
2010-05-22, by wenzelm
more Mac OS problems;
2010-05-22, by wenzelm
ignore system messages;
2010-05-22, by wenzelm
use proper ISABELLE_PLATFORM instead of adhoc uname;
2010-05-22, by wenzelm
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
removed timing;
2010-05-22, by wenzelm
rendering information and style sheets via settings;
2010-05-22, by wenzelm
more brackets -- unaligned to prevent odd auto-indentation;
2010-05-21, by wenzelm
merged
2010-05-21, by wenzelm
adjusted to changes in Mapping.thy
2010-05-21, by haftmann
merged
2010-05-21, by haftmann
tuned
2010-05-21, by haftmann
more lemmas about mappings, in particular keys
2010-05-21, by haftmann
refined
2010-05-21, by haftmann
nats in Haskell are readable
2010-05-21, by haftmann
Let rsp and prs in fun_rel/fun_map format
2010-05-21, by Cezary Kaliszyk
tuned zoom_box;
2010-05-21, by wenzelm
print calculation result in the context where the fact is actually defined -- proper externing;
2010-05-21, by wenzelm
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-05-21, by wenzelm
some message styling;
2010-05-21, by wenzelm
simplified message markup, using plain XML.Elem directly;
2010-05-21, by wenzelm
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
2010-05-21, by wenzelm
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-21, by wenzelm
bad_result: report fully explicit message;
2010-05-21, by wenzelm
observe additional isabelle-jedit.css for component and user;
2010-05-21, by wenzelm
added checkboxes for debug/tracing filter;
2010-05-21, by wenzelm
more abstract view on prover output messages;
2010-05-21, by wenzelm
added some tooltips;
2010-05-21, by wenzelm
HTML_Panel.handler as overridable method;
2010-05-21, by wenzelm
added Library.undefined (in Scala);
2010-05-21, by wenzelm
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
2010-05-21, by wenzelm
component resize: full handle_resize;
2010-05-21, by wenzelm
speed up some proofs and fix some warnings
2010-05-20, by huffman
merged
2010-05-20, by wenzelm
merged
2010-05-20, by haftmann
proper code generator for complement
2010-05-20, by haftmann
proper document text
2010-05-20, by haftmann
implement Mapping.map_entry
2010-05-20, by haftmann
operations default, map_entry, map_default; more lemmas
2010-05-20, by haftmann
added More_List.thy explicitly
2010-05-20, by haftmann
renamed List_Set to the now more appropriate More_Set
2010-05-20, by haftmann
added theory More_List
2010-05-20, by haftmann
moved generic List operations to theory More_List
2010-05-20, by haftmann
adjusted
2010-05-20, by haftmann
turned old-style mem into an input abbreviation
2010-05-20, by haftmann
zoom font size;
2010-05-20, by wenzelm
added somewhat generic zoom box;
2010-05-20, by wenzelm
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
2010-05-20, by wenzelm
mutate displayed document synchronously in Swing thread, for improved robustness;
2010-05-20, by wenzelm
read style sheets only once;
2010-05-20, by wenzelm
handle component resize for output / HTML panel;
2010-05-20, by wenzelm
Isabelle_System: allow explicit isabelle_home argument;
2010-05-20, by wenzelm
enable shell script editor mode;
2010-05-20, by wenzelm
merged
2010-05-20, by wenzelm
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