Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-1920
+1920
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
simplify definition of continuous_on; generalize some lemmas
2010-04-26, by huffman
move intervals section heading
2010-04-26, by huffman
remove unused, redundant constant inv_on
2010-04-26, by huffman
reorganize subsection headings
2010-04-26, by huffman
remove redundant lemma
2010-04-26, by huffman
more lemmas to Vec1.thy
2010-04-26, by huffman
simplify proof
2010-04-26, by huffman
move more lemmas into Vec1.thy
2010-04-26, by huffman
move proof of Fashoda meet theorem into separate file
2010-04-26, by huffman
move definitions and theorems for type real^1 to separate theory file
2010-04-26, by huffman
removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27, by wenzelm
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27, by wenzelm
really minimize sorts after certification -- looks like this is intended here;
2010-04-27, by wenzelm
tuned signature;
2010-04-27, by wenzelm
merged
2010-04-27, by wenzelm
tuned whitespace
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
fix SML/NJ compilation (I hope)
2010-04-27, by blanchet
tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27, by wenzelm
tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27, by wenzelm
tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27, by wenzelm
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27, by wenzelm
misc tuning and simplification;
2010-04-27, by wenzelm
NEWS and CONTRIBUTORS
2010-04-27, by haftmann
explicit is better than implicit
2010-04-27, by haftmann
tuned class linordered_field_inverse_zero
2010-04-27, by haftmann
merged
2010-04-27, by haftmann
instances for *_inverse_zero classes
2010-04-27, by haftmann
canonical import
2010-04-27, by haftmann
merged
2010-04-26, by haftmann
use new classes (linordered_)field_inverse_zero
2010-04-26, by haftmann
merged
2010-04-26, by blanchet
renamed option
2010-04-26, by blanchet
fixes 2a5c6e7b55cb;
2010-04-26, by blanchet
compile
2010-04-26, by blanchet
make compile (and not just load dynamically)
2010-04-26, by blanchet
merge
2010-04-26, by blanchet
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
2010-04-26, by blanchet
adapt code to reflect new signature of "neg_clausify"
2010-04-26, by blanchet
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
2010-04-26, by blanchet
rename options
2010-04-26, by blanchet
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
2010-04-26, by blanchet
remove needless code that was copy-pasted from Quickcheck (where it made sense)
2010-04-26, by blanchet
cosmetics
2010-04-25, by blanchet
cosmetics
2010-04-25, by blanchet
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-25, by blanchet
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-25, by blanchet
cosmetics: rename internal functions
2010-04-25, by blanchet
cosmetics
2010-04-25, by blanchet
remove "show_skolems" option and change style of record declarations
2010-04-25, by blanchet
remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-25, by blanchet
removed Nitpick's "uncurry" option
2010-04-24, by blanchet
fix typesetting
2010-04-24, by blanchet
Fruhjahrsputz: remove three mostly useless Nitpick options
2010-04-24, by blanchet
remove type annotations as comments;
2010-04-24, by blanchet
cosmetics
2010-04-24, by blanchet
better error reporting;
2010-04-24, by blanchet
cosmetics
2010-04-23, by blanchet
reuse timestamp function
2010-04-23, by blanchet
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-23, by blanchet
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
2010-04-23, by blanchet
remove some bloat
2010-04-23, by blanchet
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23, by blanchet
renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23, by blanchet
move the minimizer to the Sledgehammer directory
2010-04-23, by blanchet
remove debugging code
2010-04-23, by blanchet
move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23, by blanchet
give an error if no ATP is set
2010-04-23, by blanchet
move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-23, by blanchet
centralized ATP-specific error handling in "atp_wrapper.ML"
2010-04-23, by blanchet
handle ATP proof delimiters in a cleaner, more extensible fashion
2010-04-23, by blanchet
merged
2010-04-26, by wenzelm
fix another if-then-else parse error
2010-04-26, by huffman
fix if-then-else parse error
2010-04-26, by huffman
merged
2010-04-26, by huffman
fix syntax precedence declarations for UNION, INTER, SUP, INF
2010-04-26, by huffman
syntax precedence for If and Let
2010-04-26, by huffman
fix lots of looping simp calls and other warnings
2010-04-26, by huffman
fix duplicate simp rule warnings
2010-04-25, by huffman
define finer-than ordering on net type; move some theorems into Limits.thy
2010-04-25, by huffman
generalize type of continuous_on
2010-04-25, by huffman
define nets directly as filters, instead of as filter bases
2010-04-25, by huffman
use 'example_proof' (invisible);
2010-04-26, by wenzelm
command 'example_proof' opens an empty proof body;
2010-04-26, by wenzelm
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
2010-04-26, by wenzelm
eliminanated some unreferenced identifiers;
2010-04-26, by wenzelm
merged
2010-04-26, by wenzelm
add bounded_lattice_bot and bounded_lattice_top type classes
2010-04-26, by Cezary Kaliszyk
merged
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps
2010-04-26, by haftmann
class division_ring_inverse_zero
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-26, by haftmann
line break
2010-04-26, by haftmann
removed unused AxClass.class_intros;
2010-04-26, by wenzelm
updated Sign.add_type_abbrev;
2010-04-26, by wenzelm
merged
2010-04-26, by haftmann
field_simps as named theorems
2010-04-25, by haftmann
merged
2010-04-25, by wenzelm
generalize more constants and lemmas
2010-04-25, by huffman
simplify types of path operations (use real instead of real^1)
2010-04-25, by huffman
add lemmas convex_real_interval and convex_box
2010-04-25, by huffman
generalize more constants and lemmas
2010-04-24, by huffman
generalize constant closest_point
2010-04-24, by huffman
minimize imports
2010-04-24, by huffman
fix imports
2010-04-24, by huffman
document generation for Multivariate_Analysis
2010-04-24, by huffman
move l2-norm stuff into separate theory file
2010-04-24, by huffman
convert proofs to Isar-style
2010-04-24, by huffman
Library/Fraction_Field.thy: ordering relations for fractions
2010-04-24, by huffman
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-04-25, by wenzelm
more systematic treatment of data -- avoid slightly odd nested tuples here;
2010-04-25, by wenzelm
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25, by wenzelm
misc tuning and simplification;
2010-04-25, by wenzelm
simplified some private bindings;
2010-04-25, by wenzelm
classrel and arity completion by krauss/schropp;
2010-04-25, by wenzelm
removed obsolete/unused Proof.match_bind;
2010-04-25, by wenzelm
modernized naming conventions of main Isar proof elements;
2010-04-25, by wenzelm
goals: simplified handling of implicit variables -- removed obsolete warning;
2010-04-25, by wenzelm
updated generated files;
2010-04-23, by wenzelm
cover 'schematic_lemma' etc.;
2010-04-23, by wenzelm
mark schematic statements explicitly;
2010-04-23, by wenzelm
eliminated spurious schematic statements;
2010-04-23, by wenzelm
explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-23, by wenzelm
collapse category "schematic goal" in keyword table -- Proof General does not know about this;
2010-04-23, by wenzelm
added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-04-23, by wenzelm
merged
2010-04-23, by wenzelm
merged
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23, by haftmann
adapted to new times_divide_eq simp situation
2010-04-23, by haftmann
epheremal replacement of field_simps by field_eq_simps
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
2010-04-23, by haftmann
separated instantiation of division_by_zero
2010-04-23, by haftmann
dequalified fact name
2010-04-23, by haftmann
less special treatment of times_divide_eq [simp]
2010-04-23, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-23, by haftmann
more localization; tuned proofs
2010-04-23, by haftmann
more localization; factored out lemmas for division_ring
2010-04-23, by haftmann
modernized abstract algebra theories
2010-04-23, by haftmann
merged
2010-04-23, by haftmann
swapped generic code generator and SML code generator
2010-04-22, by haftmann
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
2010-04-23, by wenzelm
Item_Net/Named_Thms: export efficient member operation;
2010-04-23, by wenzelm
initialized atps reference with standard setup in the atp manager
2010-04-23, by bulwahn
compile
2010-04-23, by blanchet
handle SPASS's equality predicate correctly in Isar proof reconstruction
2010-04-23, by blanchet
merged
2010-04-23, by blanchet
added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs;
2010-04-23, by blanchet
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
2010-04-22, by blanchet
set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
2010-04-22, by blanchet
minor code cleanup
2010-04-22, by blanchet
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
2010-04-22, by blanchet
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
2010-04-22, by blanchet
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
2010-04-22, by blanchet
postprocess ATP output in "overlord" mode to make it more readable
2010-04-22, by blanchet
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
2010-04-21, by blanchet
generate command-line in addition to timestamp in ATP output file, for debugging purposes
2010-04-21, by blanchet
pass relevant options from "sledgehammer" to "sledgehammer minimize";
2010-04-21, by blanchet
Finite set theory
2010-04-23, by Cezary Kaliszyk
merged
2010-04-22, by wenzelm
Tidied up using s/l
2010-04-22, by paulson
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
2010-04-22, by wenzelm
fun_rel introduction and list_rel elimination for quotient package
2010-04-22, by Cezary Kaliszyk
lemmas concerning remdups
2010-04-22, by haftmann
lemma dlist_ext
2010-04-22, by haftmann
merged
2010-04-21, by haftmann
optionally ignore errors during translation of equations; tuned representation of abstraction points
2010-04-21, by haftmann
optionally ignore errors during translation of equations
2010-04-21, by haftmann
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
2010-04-21, by krauss
simplified example
2010-04-21, by krauss
use only one thread in "Manual_Nits";
2010-04-21, by blanchet
merged
2010-04-21, by blanchet
clarify error message
2010-04-21, by blanchet
distinguish between the different ATP errors in the user interface;
2010-04-21, by blanchet
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
2010-04-21, by blanchet
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
2010-04-20, by blanchet
merged
2010-04-21, by bulwahn
make profiling depend on reference Quickcheck.timing
2010-04-21, by bulwahn
added examples for detecting switches
2010-04-21, by bulwahn
adopting documentation of the predicate compiler
2010-04-21, by bulwahn
removing dead code; clarifying function names; removing clone
2010-04-21, by bulwahn
adopting examples to changes in the predicate compiler
2010-04-21, by bulwahn
adopting quickcheck
2010-04-21, by bulwahn
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
2010-04-21, by bulwahn
added switch detection to the predicate compiler
2010-04-21, by bulwahn
added further inlining of boolean constants to the predicate compiler
2010-04-21, by bulwahn
adding more profiling to the predicate compiler
2010-04-21, by bulwahn
only add relevant predicates to the list of extra modes
2010-04-21, by bulwahn
switched off no_topmost_reordering
2010-04-21, by bulwahn
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
2010-04-21, by bulwahn
added option for specialisation to the predicate compiler
2010-04-21, by bulwahn
prefer functional modes of functions in the mode analysis
2010-04-21, by bulwahn
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-04-21, by bulwahn
merged
2010-04-21, by hoelzl
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
2010-04-21, by hoelzl
Translated remaining theorems about integration from HOL light.
2010-04-20, by himmelma
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
2010-04-21, by wenzelm
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-04-20, by huffman
Remove garbage.
2010-04-20, by ballarin
Remove garbage.
2010-04-20, by ballarin
recovered isabelle java, which was broken in ebfa4bb0d50f;
2010-04-20, by wenzelm
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
2010-04-20, by blanchet
merged
2010-04-20, by blanchet
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-20, by blanchet
merge
2010-04-20, by blanchet
cosmetics
2010-04-19, by blanchet
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
2010-04-19, by blanchet
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19, by blanchet
added warning about inconsistent context to Metis;
2010-04-19, by blanchet
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
2010-04-19, by blanchet
got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19, by blanchet
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19, by blanchet
don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19, by blanchet
allow "_" in TPTP names in debug mode
2010-04-19, by blanchet
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-19, by blanchet
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19, by blanchet
get rid of "List.foldl" + add timestamp to SPASS
2010-04-19, by blanchet
less ambitious settings for cygwin-poly;
2010-04-20, by wenzelm
respectfullness and preservation of map for identity quotients
2010-04-20, by Cezary Kaliszyk
respectfullness and preservation of function composition
2010-04-20, by Cezary Kaliszyk
eta-normalize the goal since the original theorem is atomized
2010-04-20, by Cezary Kaliszyk
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
2010-04-20, by wenzelm
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
2010-04-20, by wenzelm
merged
2010-04-20, by haftmann
more appropriate representation of valid positions for abstractors
2010-04-19, by haftmann
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19, by haftmann
update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-04-19, by wenzelm
tuned;
2010-04-19, by wenzelm
more platform information;
2010-04-19, by wenzelm
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
2010-04-19, by wenzelm
some updates on multi-platform support;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-19, by haftmann
polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-19, by wenzelm
less ambitious settings for cygwin-poly;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
more convenient equations for zip
2010-04-19, by haftmann
more platform info;
2010-04-17, by wenzelm
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
2010-04-17, by wenzelm
system properties determine the JVM platform, not the Isabelle one;
2010-04-17, by wenzelm
THIS_CYGWIN;
2010-04-17, by wenzelm
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
2010-04-17, by wenzelm
isatest: more robust treatment of remote files, less reliance on mounted file system;
2010-04-17, by wenzelm
merged
2010-04-17, by blanchet
added missing \n in output
2010-04-17, by blanchet
by default, don't try to start ATPs that aren't installed
2010-04-16, by blanchet
fiddle with Sledgehammer option syntax
2010-04-16, by blanchet
added timestamp to proof
2010-04-16, by blanchet
restore order of clauses in TPTP output;
2010-04-16, by blanchet
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
2010-04-16, by blanchet
output total time taken by Sledgehammer if "verbose" is set
2010-04-16, by blanchet
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16, by blanchet
reorganize Sledgehammer's relevance filter slightly
2010-04-16, by blanchet
tell the user that Sledgehammer kills its siblings
2010-04-16, by blanchet
updated keywords;
2010-04-16, by wenzelm
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-16, by wenzelm
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16, by wenzelm
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16, by wenzelm
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16, by wenzelm
allow syntax types within abbreviations;
2010-04-16, by wenzelm
modernized old-style type abbreviations;
2010-04-16, by wenzelm
modernized type abbreviations;
2010-04-16, by wenzelm
local type abbreviations;
2010-04-16, by wenzelm
merged
2010-04-16, by blanchet
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16, by blanchet
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-16, by blanchet
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15, by blanchet
make Sledgehammer's output more debugging friendly
2010-04-15, by blanchet
made SML/NJ happy;
2010-04-16, by wenzelm
proper masking of dummy name_space;
2010-04-16, by wenzelm
salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;
2010-04-16, by wenzelm
proper checking of ML functors (in Poly/ML 5.2 or later);
2010-04-16, by wenzelm
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-04-16, by wenzelm
isatest: improved treatment of local files on atbroy102;
2010-04-16, by wenzelm
add rule deflation_ID to proof script for take + constructor rules
2010-04-15, by huffman
more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);
2010-04-15, by wenzelm
HOL record: explicitly allow sort constraints;
2010-04-15, by wenzelm
misc tuning and simplification;
2010-04-15, by wenzelm
explicit ProofContext.check_tfree;
2010-04-15, by wenzelm
merged
2010-04-15, by wenzelm
Respectfullness and preservation of list_rel
2010-04-15, by Cezary Kaliszyk
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
2010-04-15, by wenzelm
get_sort: suppress dummyS from input;
2010-04-15, by wenzelm
modernized treatment of sort constraints in specification;
2010-04-15, by wenzelm
typecopy: observe given sort constraints more precisely;
2010-04-15, by wenzelm
inline old Record.read_typ/cert_typ;
2010-04-15, by wenzelm
spelling;
2010-04-15, by wenzelm
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-04-15, by haftmann
tuned whitespace;
2010-04-14, by wenzelm
merged
2010-04-14, by wenzelm
merged
2010-04-14, by blanchet
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-04-14, by blanchet
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-04-14, by blanchet
make Sledgehammer's "timeout" option work for "minimize"
2010-04-14, by blanchet
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
2010-04-14, by blanchet
Spelling error: theroems -> theorems
2010-04-14, by hoelzl
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
2010-04-14, by krauss
record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
2010-04-14, by krauss
more precise treatment of UNC server prefix, e.g. //foo;
2010-04-14, by wenzelm
support named_root, which approximates UNC server prefix (for Cygwin);
2010-04-14, by wenzelm
updated Thm.add_axiom/add_def;
2010-04-14, by wenzelm
adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;
2010-04-14, by wenzelm
bring HOLCF/ex/Domain_Proofs.thy up to date
2010-04-13, by huffman
adapt Refute example to reflect latest soundness fix to Refute
2010-04-13, by blanchet
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
2010-04-13, by blanchet
merged
2010-04-13, by blanchet
make Nitpick output everything to tracing in debug mode;
2010-04-13, by blanchet
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
2010-04-13, by blanchet
cosmetics
2010-04-13, by blanchet
merge
2010-04-13, by Cezary Kaliszyk
merge
2010-04-13, by Cezary Kaliszyk
add If respectfullness and preservation to Quotient package database
2010-04-13, by Cezary Kaliszyk
more accurate pattern match
2010-04-13, by haftmann
dropped dead code
2010-04-13, by haftmann
update domain package examples
2010-04-12, by huffman
remove dead code
2010-04-12, by huffman
share more code between definitional and axiomatic domain packages
2010-04-12, by huffman
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
2010-04-12, by huffman
Changed the type of Quot_True, so that it is an HOL constant.
2010-04-12, by Cezary Kaliszyk
removed rather toyish tree
2010-04-11, by haftmann
updated keywords
2010-04-11, by haftmann
merged
2010-04-11, by haftmann
user interface for abstract datatypes is an attribute, not a command
2010-04-11, by haftmann
implementation of mappings by rbts
2010-04-11, by haftmann
lemma is_empty_empty
2010-04-11, by haftmann
constructor Mapping replaces AList
2010-04-11, by haftmann
stay within Local_Defs layer;
2010-04-11, by wenzelm
expose foundational typedef axiom name;
2010-04-11, by wenzelm
Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-04-11, by wenzelm
modernized datatype constructors;
2010-04-11, by wenzelm
of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
2010-04-11, by wenzelm
tuned;
2010-04-11, by wenzelm
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-04-11, by wenzelm
include JEDIT_APPLE_PROPERTIES by default;
2010-04-09, by wenzelm
isatest: more uniform setup for Unix vs. Cygwin;
2010-04-09, by wenzelm
added missing case: meta universal quantifier
2010-04-08, by boehmes
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
2010-04-08, by bulwahn
Merged.
2010-04-07, by ballarin
Merged resolving conflicts NEWS and locale.ML.
2010-04-07, by ballarin
Proper inheritance of mixins for activated facts and locale dependencies.
2010-04-02, by ballarin
Removed obsolete function.
2010-02-15, by ballarin
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-02-15, by ballarin
Tuned interpretation proofs.
2010-02-15, by ballarin
A rough implementation of full mixin inheritance; additional unit tests.
2010-02-11, by ballarin
Clarified invariant; tuned.
2010-02-02, by ballarin
More mixin tests.
2010-02-01, by ballarin
Use serial to be more debug friendly.
2010-02-01, by ballarin
buffered output (faster than direct output)
2010-04-07, by boehmes
simplified Cache_IO interface (input is just a string and not already stored in a file)
2010-04-07, by boehmes
shortened interface (do not export unused options and functions)
2010-04-07, by boehmes
always unfold definitions of specific constants (including special binders)
2010-04-07, by boehmes
shorten the code by conditional function application
2010-04-07, by boehmes
fail for problems containg the universal sort (as those problems cannot be atomized)
2010-04-07, by boehmes
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
2010-04-07, by boehmes
Added Information theory and Example: dining cryptographers
2010-04-07, by hoelzl
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
2010-04-07, by Christian Urban
removed (latex output) notation which is sometimes very ugly
2010-04-06, by krauss
merged
2010-04-06, by boehmes
added missing mult_1_left to linarith simp rules
2010-04-06, by boehmes
tuned proof (no induction needed); removed unused lemma and fuzzy comment
2010-04-06, by krauss
isatest: basic setup for cygwin-poly on atbroy102;
2010-04-02, by wenzelm
slightly more standard dependencies;
2010-04-01, by wenzelm
merged
2010-04-01, by nipkow
tuned many proofs a bit
2010-04-01, by nipkow
merged
2010-04-01, by nipkow
documented [[trace_simp=true]]
2010-03-29, by nipkow
add missing goal argument
2010-04-01, by blanchet
adapt syntax of Sledgehammer options in examples
2010-04-01, by blanchet
merged
2010-04-01, by blanchet
fixed layout of Sledgehammer output
2010-04-01, by blanchet
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29, by blanchet
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29, by blanchet
get rid of Polyhash, since it's no longer used
2010-03-29, by blanchet
remove use of Polyhash;
2010-03-29, by blanchet
reintroduce efficient set structure to collect "no_atp" theorems
2010-03-29, by blanchet
made "theory_const" a Sledgehammer option;
2010-03-29, by blanchet
added "respect_no_atp" and "convergence" options to Sledgehammer;
2010-03-29, by blanchet
adding MREC induction rule in Imperative HOL
2010-03-31, by bulwahn
made smlnj happy
2010-03-31, by bulwahn
adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned
2010-03-31, by bulwahn
adopting specialisation examples to moving the alternative defs in the library
2010-03-31, by bulwahn
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
2010-03-31, by bulwahn
no specialisation for predicates without introduction rules in the predicate compiler
2010-03-31, by bulwahn
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
2010-03-31, by bulwahn
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
2010-03-31, by bulwahn
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-31, by bulwahn
clarifying the Predicate_Compile_Core signature
2010-03-31, by bulwahn
adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure
2010-03-31, by bulwahn
putting compilation setup of predicate compiler in a separate file
2010-03-31, by bulwahn
simplify fold_graph proofs
2010-03-30, by huffman
NEWS
2010-03-30, by krauss
removed dead code; fixed typo
2010-03-30, by krauss
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
2010-03-30, by krauss
merged
2010-03-30, by wenzelm
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
2010-03-29, by bulwahn
tuned
2010-03-29, by bulwahn
generalized alternative functions to alternative compilation to handle arithmetic functions better
2010-03-29, by bulwahn
correcting alternative functions with tuples
2010-03-29, by bulwahn
no specialisation for patterns with only tuples in the predicate compiler
2010-03-29, by bulwahn
adding registration of functions in the function flattening
2010-03-29, by bulwahn
added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
2010-03-29, by bulwahn
adding specialisation examples of the predicate compiler
2010-03-29, by bulwahn
adding specialisation of predicates to the predicate compiler
2010-03-29, by bulwahn
returning an more understandable user error message in the values command
2010-03-29, by bulwahn
adding Lazy_Sequences with explicit depth-bound
2010-03-29, by bulwahn
removing fishing for split thm in the predicate compiler
2010-03-29, by bulwahn
prefer recursive calls before others in the mode inference
2010-03-29, by bulwahn
added statistics to values command for random generation
2010-03-29, by bulwahn
adopting Predicate_Compile_Quickcheck
2010-03-29, by bulwahn
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
2010-03-29, by bulwahn
removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
2010-03-29, by bulwahn
adding a hook for experiments in the predicate compilation process
2010-03-29, by bulwahn
removing simple equalities in introduction rules in the predicate compiler
2010-03-29, by bulwahn
adopting Predicate_Compile
2010-03-29, by bulwahn
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-03-29, by bulwahn
generalizing the compilation process of the predicate compiler
2010-03-29, by bulwahn
added new compilation to predicate_compiler
2010-03-29, by bulwahn
adding new depth-limited and new random monad for the predicate compiler
2010-03-29, by bulwahn
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
adapted to Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
auto update by Netbeans 6.8;
2010-03-30, by wenzelm
adapted to Netbeans 6.8 and Scala for Netbeans 6.8v1.1;
2010-03-30, by wenzelm
replaced some deprecated methods;
2010-03-29, by wenzelm
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
2010-03-29, by wenzelm
merged
2010-03-29, by huffman
use lattice theorems to prove set theorems
2010-03-28, by huffman
add/change some lemmas about lattices
2010-03-28, by huffman
cleaned up some proofs
2010-03-28, by huffman
the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
2010-03-29, by boehmes
merged
2010-03-28, by wenzelm
implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
2010-03-28, by wenzelm
make SML/NJ happy
2010-03-28, by blanchet
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28, by wenzelm
static defaults for configuration options;
2010-03-28, by wenzelm
configuration options admit dynamic default values;
2010-03-28, by wenzelm
tuned;
2010-03-28, by wenzelm
do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
2010-03-28, by wenzelm
use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
2010-03-28, by wenzelm
merged
2010-03-27, by wenzelm
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
2010-03-27, by boehmes
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-27, by wenzelm
merged
2010-03-27, by nipkow
added reference to Trace Simp Depth.
2010-03-27, by nipkow
merged
2010-03-27, by wenzelm
Automated lifting can be restricted to specific quotient types
2010-03-27, by Cezary Kaliszyk
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-03-27, by wenzelm
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
2010-03-27, by wenzelm
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
2010-03-27, by wenzelm
added Term.fold_atyps_sorts convenience;
2010-03-27, by wenzelm
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-27, by wenzelm
eliminated old-style Theory.add_defs_i;
2010-03-27, by wenzelm
slightly more general simproc (avoids errors of linarith)
2010-03-27, by boehmes
merged
2010-03-27, by boehmes
updated SMT certificates
2010-03-26, by boehmes
made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
2010-03-26, by boehmes
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-26, by boehmes
merged
2010-03-26, by wenzelm
Added finite measure space.
2010-03-26, by hoelzl
tuned white space;
2010-03-26, by wenzelm
more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
2010-03-26, by wenzelm
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
2010-03-26, by wenzelm
merged
2010-03-25, by wenzelm
merged
2010-03-25, by blanchet
make Mirabelle happy again
2010-03-25, by blanchet
revert debugging output that shouldn't have been submitted in the first place
2010-03-24, by blanchet
added support for Sledgehammer parameters;
2010-03-24, by blanchet
simplify Nitpick parameter parsing code a little bit + make compile
2010-03-24, by blanchet
add new file "sledgehammer_util.ML" to setup
2010-03-24, by blanchet
honor the newly introduced Sledgehammer parameters and fixed the parsing;
2010-03-24, by blanchet
added a syntax for specifying facts to Sledgehammer;
2010-03-23, by blanchet
leverage code now in Sledgehammer
2010-03-23, by blanchet
added options to Sledgehammer;
2010-03-23, by blanchet
make "sledgehammer" and "atp_minimize" improper commands
2010-03-22, by blanchet
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
2010-03-25, by wenzelm
removed unused AxClass.of_sort derivation;
2010-03-25, by wenzelm
more precise dependencies;
2010-03-24, by wenzelm
merged
2010-03-24, by wenzelm
merged
2010-03-24, by bulwahn
removed predicate_compile_core.ML from HOL-ex session
2010-03-24, by bulwahn
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
2010-03-24, by bulwahn
adopting examples to Library move
2010-03-24, by bulwahn
moved further predicate compile files to HOL-Library
2010-03-24, by bulwahn
added simple setup for arithmetic on natural numbers
2010-03-24, by bulwahn
removing uncommented examples in setup theory of predicate compile quickcheck
2010-03-24, by bulwahn
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
2010-03-24, by bulwahn
slightly more logical bootstrap order -- also helps to sort out proof terms extension;
2010-03-24, by wenzelm
remove ancient continuity tactic
2010-03-24, by huffman
removed Cache_IO component
2010-03-24, by boehmes
updated SMT certificates
2010-03-24, by boehmes
inhibit invokation of external SMT solver
2010-03-24, by boehmes
more precise dependencies
2010-03-24, by boehmes
cache_io is now just a single ML file instead of a component
2010-03-24, by boehmes
use internal SHA1 digest implementation for generating hash keys
2010-03-24, by boehmes
remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)
2010-03-24, by boehmes
merged
2010-03-23, by huffman
minimize dependencies
2010-03-23, by huffman
sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
2010-03-23, by huffman
use ml_platform instead of ml_system to distinguish library names
2010-03-23, by boehmes
merged
2010-03-23, by boehmes
use LONG rather than INT to represent the C datatype size_t
2010-03-23, by boehmes
merged
2010-03-23, by wenzelm
remove continuous let-binding function CLet; add cont2cont rule ordinary Let
2010-03-23, by huffman
move letrec stuff to new file HOLCF/ex/Letrec.thy
2010-03-23, by huffman
more accurate dependencies;
2010-03-23, by wenzelm
even less ambitious isatest for smlnj;
2010-03-23, by wenzelm
Unhide measure_space.positive defined in Caratheodory.
2010-03-23, by hoelzl
Generate image for HOL-Probability
2010-03-23, by hoelzl
updated Thm.add_axiom/add_def;
2010-03-23, by wenzelm
completely remove constants cpair, cfst, csnd
2010-03-22, by huffman
use Pair instead of cpair in Fixrec_ex.thy
2010-03-22, by huffman
use Pair instead of cpair
2010-03-22, by huffman
define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd
2010-03-22, by huffman
define csplit using fst, snd
2010-03-22, by huffman
convert lemma fix_cprod to use Pair, fst, snd
2010-03-22, by huffman
remove unused syntax for as_pat, lazy_pat
2010-03-22, by huffman
add lemmas fst_monofun, snd_monofun
2010-03-22, by huffman
use Pair instead of cpair
2010-03-22, by huffman
use fixrec_simp instead of fixpat
2010-03-22, by huffman
use Pair, fst, snd instead of cpair, cfst, csnd
2010-03-22, by huffman
remove admw predicate
2010-03-22, by huffman
remove contlub predicate
2010-03-22, by huffman
merged
2010-03-22, by huffman
error -> raise Fail
2010-03-22, by huffman
merged
2010-03-22, by wenzelm
merged
2010-03-22, by wenzelm
merged
2010-03-22, by wenzelm
remove unused adm_tac.ML
2010-03-22, by huffman
avoid dependence on adm_tac solver
2010-03-22, by huffman
remove obsolete holcf_logic.ML
2010-03-22, by huffman
fix ML warning in domain_library.ML
2010-03-22, by huffman
fix ML warnings in repdef.ML
2010-03-22, by huffman
fix ML warnings in fixrec.ML
2010-03-22, by huffman
fix ML warnings in pcpodef.ML
2010-03-22, by huffman
fix LaTeX overfull hbox warnings in HOLCF document
2010-03-22, by huffman
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-22, by huffman
explicit Simplifier.global_context;
2010-03-22, by wenzelm
recovered header;
2010-03-22, by wenzelm
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22, by wenzelm
inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
2010-03-22, by wenzelm
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
2010-03-22, by wenzelm
added Specification.axiom convenience;
2010-03-22, by wenzelm
detect OFCLASS() axioms in Nitpick;
2010-03-22, by blanchet
merged
2010-03-22, by bulwahn
contextifying the compilation of the predicate compiler
2010-03-22, by bulwahn
removed unused Predicate_Compile_Set
2010-03-22, by bulwahn
avoiding fishing for split_asm rule in the predicate compiler
2010-03-22, by bulwahn
contextifying the proof procedure in the predicate compiler
2010-03-22, by bulwahn
making flat triples to nested tuple to remove general triple functions
2010-03-22, by bulwahn
reduced the debug output functions from 2 to 1
2010-03-22, by bulwahn
some improvements thanks to Makarius source code review
2010-03-22, by bulwahn
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
2010-03-22, by bulwahn
enabling a previously broken example of the predicate compiler again
2010-03-22, by bulwahn
improving handling of case expressions in predicate rewriting
2010-03-22, by bulwahn
adding depth_limited_random compilation to predicate compiler
2010-03-22, by bulwahn
a new simpler random compilation for the predicate compiler
2010-03-22, by bulwahn
reviving the classical depth-limited computation in the predicate compiler
2010-03-22, by bulwahn
cleaning the function flattening
2010-03-22, by bulwahn
generalized split transformation in the function flattening
2010-03-22, by bulwahn
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
2010-03-22, by bulwahn
restructuring function flattening
2010-03-22, by bulwahn
renaming mk_prems to flatten in the function flattening
2010-03-22, by bulwahn
simplifying function flattening
2010-03-22, by bulwahn
removed warning_count (known causes for warnings have been resolved)
2010-03-22, by boehmes
remove the iteration counter from Sledgehammer's minimizer
2010-03-22, by blanchet
merged
2010-03-22, by blanchet
start work on direct proof reconstruction for Sledgehammer
2010-03-22, by blanchet
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
2010-03-19, by blanchet
move all ATP setup code into ATP_Wrapper
2010-03-19, by blanchet
move the Sledgehammer Isar commands together into one file;
2010-03-19, by blanchet
more Sledgehammer refactoring
2010-03-19, by blanchet
use a proof context instead of a local theory
2010-03-22, by boehmes
provide a hook to safely manipulate verification conditions
2010-03-22, by boehmes
replaced old-style Drule.add_axiom by Specification.axiomatization
2010-03-22, by boehmes
removed e-mail address from error message
2010-03-22, by boehmes
merged
2010-03-22, by haftmann
tuned whitespace
2010-03-21, by haftmann
handle hidden polymorphism in class target (without class target syntax, though)
2010-03-21, by haftmann
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-22, by wenzelm
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-22, by wenzelm
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
2010-03-21, by wenzelm
Logic.mk_of_sort convenience;
2010-03-21, by wenzelm
more explicit invented name;
2010-03-21, by wenzelm
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-21, by wenzelm
do not open ML structures;
2010-03-21, by wenzelm
modernized overloaded definitions;
2010-03-21, by wenzelm
standard headers;
2010-03-21, by wenzelm
slightly more uniform definitions -- eliminated old-style meta-equality;
2010-03-21, by wenzelm
eliminated old constdefs;
2010-03-21, by wenzelm
corrected setup for of_list
2010-03-21, by haftmann
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-20, by wenzelm
added lemma infinite_Un
2010-03-20, by Christian Urban
Check that argument is not a 'Bound' before calling fastype_of.
2010-03-19, by Cezary Kaliszyk
typedef etc.: no constraints;
2010-03-19, by wenzelm
allow sort constraints in HOL/typedef;
2010-03-19, by wenzelm
allow sort constraints in HOL/typedef and related HOLCF variants;
2010-03-19, by wenzelm
OuterParse.type_args_constrained;
2010-03-19, by wenzelm
support type arguments with sort constraints;
2010-03-19, by wenzelm
typedecl: no sort constraints;
2010-03-18, by wenzelm
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
2010-03-18, by wenzelm
typedecl: no sort constraints;
2010-03-18, by wenzelm
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
2010-03-18, by wenzelm
Added product measure space
2010-03-16, by hoelzl
added type constraints to make SML/NJ happy
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
fix Mirabelle after renaming Sledgehammer structures
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18, by blanchet
renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17, by blanchet
renamed Sledgehammer structures
2010-03-17, by blanchet
move Sledgehammer files in a directory of their own
2010-03-17, by blanchet
merged
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
lemma swap_inj_on, swap_product
2010-03-18, by haftmann
meaningful transfer certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
2010-03-18, by haftmann
updated certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
added locales folding_one_(idem); various streamlining and tuning
2010-03-18, by haftmann
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-17, by boehmes
added one-entry cache around Kodkod invocation
2010-03-17, by blanchet
merged
2010-03-17, by blanchet
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
2010-03-17, by blanchet
minor additions to Nitpick docs
2010-03-17, by blanchet
NEWS: Nat_Bijection library
2010-03-17, by huffman
document "nitpick_choice_spec" attribute
2010-03-17, by blanchet
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
2010-03-17, by blanchet
added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-17, by blanchet
rollback of local typedef until problem with type-variables can be sorted out; fixed header
2010-03-16, by Christian Urban
adjusted to changes in Finite_Set
2010-03-16, by haftmann
merged
2010-03-15, by wenzelm
merged
2010-03-15, by nipkow
tuned inductions
2010-03-15, by nipkow
tuned;
2010-03-15, by wenzelm
moved old Sign.intern_term to the place where it is still used;
2010-03-15, by wenzelm
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-15, by wenzelm
replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-15, by wenzelm
merged
2010-03-15, by haftmann
corrected disastrous syntax declarations
2010-03-15, by haftmann
added stmaryrd for isasymSqinter
2010-03-15, by haftmann
use headers consistently
2010-03-14, by huffman
no_document for theory Countable
2010-03-14, by huffman
old domain package also defines map functions
2010-03-14, by huffman
separate map-related code into new function define_map_functions
2010-03-14, by huffman
removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14, by Christian Urban
tuned comment;
2010-03-14, by wenzelm
observe standard header format;
2010-03-14, by wenzelm
expose formal text;
2010-03-14, by wenzelm
localized @{class} and @{type};
2010-03-14, by wenzelm
move functions into holcf_library.ML
2010-03-14, by huffman
simplify definition of when combinators
2010-03-14, by huffman
declare case_names for various induction rules
2010-03-13, by huffman
add case name 'adm' for infinite induction rules
2010-03-13, by huffman
renamed some lemmas generated by the domain package
2010-03-13, by huffman
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
2010-03-13, by huffman
fixpat command prints legacy_feature warning
2010-03-13, by huffman
merged
2010-03-13, by huffman
pass binding as argument to add_domain_constructors; proper binding for case combinator
2010-03-13, by huffman
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
2010-03-13, by huffman
pass take_info as argument to Domain_Theorems.theorems
2010-03-13, by huffman
replace some string arguments with bindings
2010-03-13, by huffman
more consistent use of qualified bindings
2010-03-13, by huffman
avoid unnecessary primed variable names
2010-03-13, by huffman
remove redundant lemmas
2010-03-13, by huffman
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
2010-03-13, by huffman
fixrec now generates qualified theorem names
2010-03-13, by huffman
no_document for Infinite_Set in HOLCF
2010-03-13, by huffman
removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-13, by wenzelm
Local_Theory.define handles hidden polymorphism;
2010-03-13, by wenzelm
local theory specifications handle hidden polymorphism implicitly;
2010-03-13, by wenzelm
minor tuning and simplification;
2010-03-13, by wenzelm
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
2010-03-13, by wenzelm
removed old CVS Ids;
2010-03-13, by wenzelm
reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
2010-03-13, by wenzelm
merged
2010-03-13, by wenzelm
merged
2010-03-12, by bulwahn
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
2010-03-12, by bulwahn
adding Spec_Rules to definitional package inductive and inductive_set
2010-03-12, by bulwahn
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-03-12, by bulwahn
merged
2010-03-12, by nipkow
Reorganized Hoare logic theories; added Hoare_Den
2010-03-12, by nipkow
merged
2010-03-12, by hoelzl
reset smt_certificates
2010-03-09, by himmelma
added lemmas
2010-03-09, by himmelma
merged
2010-03-12, by nipkow
Added Hoare_Op.thy
2010-03-12, by nipkow
Equality of integral and infinite sum.
2010-03-12, by hoelzl
make tests less demanding, to prevent sporadic failures
2010-03-12, by blanchet
more antiquotations;
2010-03-13, by wenzelm
command 'typedef' now works within a local theory context;
2010-03-13, by wenzelm
removed obsolete HOL 'typedecl';
2010-03-13, by wenzelm
adapted to localized typedef: handle single global interpretation only;
2010-03-13, by wenzelm
global typedef;
2010-03-13, by wenzelm
localized typedef;
2010-03-13, by wenzelm
added typedecl_wrt, which affects default sorts of type args;
2010-03-13, by wenzelm
Local_Defs.contract convenience;
2010-03-13, by wenzelm
added Local_Theory.alias operations (independent of target);
2010-03-13, by wenzelm
merged
2010-03-11, by wenzelm
merged
2010-03-11, by nipkow
converted proofs to Isar
2010-03-11, by nipkow
merged
2010-03-11, by haftmann
merged
2010-03-11, by haftmann
tuned prefix of ac rules
2010-03-11, by haftmann
deleted default simp rule card.insert
2010-03-11, by haftmann
updated generated certificate
2010-03-11, by haftmann
replaced card_def by card_eq_setsum
2010-03-11, by haftmann
NEWS
2010-03-11, by haftmann
Big_Operators now in Main rather than Plain
2010-03-11, by haftmann
tuned prefixes of ac interpretations
2010-03-11, by haftmann
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
2010-03-11, by haftmann
fixed typo
2010-03-11, by haftmann
tuned monoid locales and prefix of sublocale interpretations
2010-03-11, by haftmann
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
2010-03-11, by haftmann
fixed typo
2010-03-11, by haftmann
added locales for monoids
2010-03-10, by haftmann
split off theory Big_Operators from theory Finite_Set
2010-03-10, by haftmann
moved some Nitpick code around
2010-03-11, by blanchet
more basic Local_Defs.export_cterm;
2010-03-11, by wenzelm
tuned signature;
2010-03-11, by wenzelm
tuned;
2010-03-11, by wenzelm
actually apply morphism to binding;
2010-03-11, by wenzelm
absolute lib_path relative to ML_HOME -- for improved robustness;
2010-03-11, by wenzelm
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-03-11, by blanchet
added term postprocessor to Nitpick, to provide custom syntax for typedefs
2010-03-11, by blanchet
made "Manual_Nits" tests more robust
2010-03-11, by blanchet
merged
2010-03-11, by haftmann
made smlnj happy
2010-03-11, by haftmann
replace Nat_Int_Bij with Nat_Bijection in ROOT.ML
2010-03-10, by huffman
remove obsolete theory Nat_Int_Bij
2010-03-10, by huffman
switch from Nat_Int_Bij to Nat_Bijection
2010-03-10, by huffman
convert HOL-Probability to use Nat_Bijection library
2010-03-10, by huffman
convert SET_Protocol to use Nat_Bijection library
2010-03-10, by huffman
convert TLS to use Nat_Bijection library
2010-03-10, by huffman
adapt HOLCF to use Nat_Bijection library
2010-03-10, by huffman
new theory Library/Nat_Bijection.thy
2010-03-10, by huffman
improve precision of "card" in Nitpick
2010-03-10, by blanchet
merged
2010-03-10, by blanchet
merged
2010-03-10, by blanchet
show nice error message in Nitpick when "java" is not available
2010-03-10, by blanchet
fixed soundness bug in Nitpick
2010-03-10, by blanchet
merged
2010-03-10, by hoelzl
Use same order of neq-elimination as in proof search.
2010-03-09, by hoelzl
Moved theorems in Lebesgue to the right places
2010-03-08, by hoelzl
constdefs is legacy
2010-03-10, by haftmann
recdef is legacy
2010-03-10, by haftmann
fixed typo
2010-03-10, by haftmann
avoid confusion
2010-03-10, by haftmann
tuned whitespace
2010-03-10, by haftmann
merged
2010-03-10, by haftmann
tuned
2010-03-10, by haftmann
clarified transfer code proper; more natural declaration of return rules
2010-03-09, by haftmann
misc tuning
2010-03-09, by haftmann
Typedecl.typedecl_global;
2010-03-09, by wenzelm
localized typedecl;
2010-03-09, by wenzelm
aliases for class/type/const;
2010-03-09, by wenzelm
added Name_Space.alias -- additional accesses for an existing entry;
2010-03-09, by wenzelm
merged
2010-03-09, by wenzelm
merged
2010-03-09, by haftmann
data administration using canonical functorial operations
2010-03-09, by haftmann
tuned data structures; using AList.map_default
2010-03-09, by haftmann
consistent field names; tuned interface
2010-03-09, by haftmann
weakend class ring_div; tuned
2010-03-09, by haftmann
more work on Nitpick's finite sets
2010-03-09, by blanchet
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09, by blanchet
ProofContext.read_class/read_type_name_proper;
2010-03-09, by wenzelm
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-03-09, by wenzelm
simplified Syntax.basic_syntax (again);
2010-03-09, by wenzelm
tuned -- eliminated Sign.intern_sort;
2010-03-09, by wenzelm
renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
2010-03-09, by wenzelm
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-03-09, by blanchet
merged
2010-03-08, by huffman
remove unnecessary error handling code
2010-03-08, by huffman
construct fully typed goal in proof of induction rule
2010-03-08, by huffman
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
2010-03-08, by huffman
remove redundant function arguments
2010-03-08, by huffman
include take_info within take_induct_info type
2010-03-08, by huffman
pass take_info as an argument to comp_theorems
2010-03-08, by huffman
pass take_induct_info as an argument to comp_theorems
2010-03-08, by huffman
add type take_induct_info
2010-03-08, by huffman
generate take_induct lemmas
2010-03-08, by huffman
move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-08, by huffman
move lemmas from Domain.thy to Domain_Aux.thy
2010-03-08, by huffman
move take-proofs stuff into new theory Domain_Aux.thy
2010-03-08, by huffman
add type take_info
2010-03-08, by huffman
add function add_qualified_def
2010-03-08, by huffman
merged
2010-03-08, by haftmann
proper ML interface; further polishing
2010-03-08, by haftmann
code simplification and tuning
2010-03-08, by haftmann
Added inducts field to inductive_result.
2010-03-08, by berghofe
transfer: avoid camel case, more standard coding conventions, misc tuning
2010-03-08, by haftmann
transfer: avoid camel case
2010-03-08, by haftmann
merged
2010-03-07, by huffman
generate separate qualified theorem name for each type's reach and take_lemma
2010-03-07, by huffman
add simp rule LAM_strict
2010-03-07, by huffman
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
2010-03-07, by huffman
merged
2010-03-07, by haftmann
dropped dead code; adhere more closely to standard coding conventions
2010-03-07, by haftmann
merged
2010-03-07, by huffman
arith tactic uses 'priority' instead of 'warning' to print messages
2010-03-07, by huffman
add simp rules about Ints, Nats
2010-03-07, by huffman
add more simp rules for Ints
2010-03-07, by huffman
add lemmas Nats_cases and Nats_induct
2010-03-07, by huffman
generalize some lemmas, and remove a few unnecessary ones
2010-03-07, by huffman
generalize some lemmas from class linordered_ring_strict to linordered_ring
2010-03-06, by huffman
add case_names attribute to casedist and ind rules
2010-03-06, by huffman
add some lemmas about complete lattices
2010-03-06, by huffman
Digesting strings according to SHA-1.
2010-03-07, by wenzelm
proper int wrapping for Word32;
2010-03-07, by wenzelm
separate structure Typedecl;
2010-03-07, by wenzelm
modernized structure Object_Logic;
2010-03-07, by wenzelm
modernized structure Local_Defs;
2010-03-07, by wenzelm
merged
2010-03-06, by paulson
merged
2010-03-06, by paulson
simplified
2010-03-06, by paulson
merged
2010-03-06, by haftmann
lemma restrict_complement_singleton_eq
2010-03-06, by haftmann
some lemma refinements
2010-03-06, by haftmann
added Table.thy
2010-03-06, by haftmann
provide ProofContext.def_type depending on "pattern" mode;
2010-03-06, by wenzelm
record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
2010-03-06, by wenzelm
record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
2010-03-06, by wenzelm
eliminated Args.bang_facts (legacy feature);
2010-03-06, by wenzelm
eliminated old-style prems;
2010-03-06, by wenzelm
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
2010-03-06, by wenzelm
Some notes on platform support of Isabelle.
2010-03-06, by wenzelm
"private" map_of_map lemma
2010-03-06, by haftmann
added insort_insert
2010-03-06, by haftmann
added dom_option_map, map_of_map_keys
2010-03-06, by haftmann
added bulkload; tuned document
2010-03-06, by haftmann
merged
2010-03-06, by haftmann
merged
2010-03-05, by haftmann
moved lemma map_sorted_distinct_set_unique
2010-03-05, by haftmann
various refinements
2010-03-05, by haftmann
print message when finiteness of domain definition is detected
2010-03-05, by huffman
merged
2010-03-05, by huffman
skip coinduction proofs for indirect-recursive domain definitions
2010-03-05, by huffman
merged
2010-03-06, by wenzelm
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
2010-03-05, by huffman
add comment
2010-03-05, by huffman
move take_proofs-related stuff to a new section
2010-03-05, by huffman
remove dead code
2010-03-05, by huffman
tuned dead code;
2010-03-05, by wenzelm
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
2010-03-05, by wenzelm
merged
2010-03-05, by wenzelm
fix proof script so 'domain foo = Foo foo' works
2010-03-05, by huffman
fix proof script so qdomain_isomorphism foo = foo' works
2010-03-05, by huffman
finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
2010-03-05, by wenzelm
isabelle browser -b: Admin/build only;
2010-03-05, by wenzelm
merged
2010-03-05, by huffman
skip proof of induction rule for indirect-recursive domain definitions
2010-03-05, by huffman
generalized inj_uminus; added strict_mono_imp_inj_on
2010-03-05, by hoelzl
merged
2010-03-05, by hoelzl
Add Lebesgue integral and probability space.
2010-03-04, by hoelzl
Supremum and Infimum on real intervals
2010-03-04, by hoelzl
Rewrite rules for images of minus of intervals
2010-03-04, by hoelzl
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
2010-03-04, by hoelzl
Added natfloor and floor rules for multiplication and power.
2010-03-04, by hoelzl
Generalized setsum_cases
2010-03-04, by hoelzl
Added vimage_inter_cong
2010-03-04, by hoelzl
merged
2010-03-04, by huffman
move coinduction-related stuff into function prove_coindunction
2010-03-04, by huffman
add function add_qualified_simp_thm
2010-03-04, by huffman
generate lemma take_below, declare chain_take [simp]
2010-03-03, by huffman
switch to polyml-svn;
2010-03-04, by wenzelm
basic simplification of external_prover signature;
2010-03-04, by wenzelm
tuned;
2010-03-04, by wenzelm
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
2010-03-04, by wenzelm
point to http://hginit.com/
2010-03-04, by wenzelm
Simplified a couple of proofs and corrected a comment
2010-03-04, by paulson
lemmas set_map_of_compr, map_of_inject_set
2010-03-04, by haftmann
merged
2010-03-03, by huffman
merged
2010-03-03, by huffman
remove dead code
2010-03-03, by huffman
add infix declarations
2010-03-03, by huffman
remove unnecessary theorem references
2010-03-03, by huffman
remove copy_of_dtyp from domain_axioms.ML
2010-03-03, by huffman
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
2010-03-03, by huffman
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03, by huffman
add function axiomatize_lub_take
2010-03-03, by huffman
move function mk_lub into holcf_library.ML
2010-03-03, by huffman
added extern_syntax;
2010-03-03, by wenzelm
merged
2010-03-03, by haftmann
more uniform naming conventions
2010-03-03, by haftmann
tuned whitespace
2010-03-03, by haftmann
restructured RBT theory
2010-03-03, by haftmann
stats for at-poly-test;
2010-03-03, by wenzelm
proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);
2010-03-03, by wenzelm
merged, resolving some basic conflicts;
2010-03-03, by wenzelm
merged
2010-03-03, by krauss
updated patch for hgweb style: now applies to Mercurial 1.4.3 templates
2010-03-03, by krauss
fix fragile proof using old induction rule (cf. bdf8ad377877)
2010-03-03, by krauss
merged
2010-03-03, by hoelzl
replaced \<bullet> with inner
2010-03-02, by himmelma
tuned
2010-03-02, by himmelma
the ordering on real^1 is linear
2010-03-02, by himmelma
merged
2010-03-03, by bulwahn
made smlnj happy
2010-03-02, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-03-02, by bulwahn
adding HOL-Mutabelle to tests
2010-03-02, by bulwahn
merged
2010-03-03, by haftmann
more explicit naming scheme
2010-03-03, by haftmann
merged
2010-03-02, by huffman
adapt to changed variable name in casedist theorem
2010-03-02, by huffman
remove dependency on domain_syntax.ML
2010-03-02, by huffman
update HOLCF makefile
2010-03-02, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02, by huffman
proof scripts use variable name y for casedist
2010-03-02, by huffman
fixrec and repdef modules import holcf_library
2010-03-02, by huffman
use y as variable name in casedist, like datatype package
2010-03-02, by huffman
proper names for types cfun, sprod, ssum
2010-03-02, by huffman
variable name changed
2010-03-02, by huffman
fix proof script for take_apps so it works with indirect recursion
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
remove unused mixfix component from type cons
2010-03-02, by huffman
cleaned up, added type annotations
2010-03-02, by huffman
remove unused selector field from type arg
2010-03-02, by huffman
add_syntax no longer needs a definitional mode
2010-03-02, by huffman
add_axioms no longer needs a definitional mode
2010-03-02, by huffman
get rid of primes on thy variables
2010-03-02, by huffman
move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02, by huffman
move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02, by huffman
remove map_tab argument to calc_axioms
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
merged
2010-03-02, by paulson
Slightly generalised a theorem
2010-03-02, by paulson
merged
2010-03-02, by paulson
merged
2010-02-19, by paulson
merged
2010-02-19, by paulson
merged
2010-02-05, by paulson
merged
2010-02-04, by paulson
merged
2010-02-02, by paulson
Correction of a tiny error
2010-02-02, by paulson
removed obsolete helper theory
2010-03-02, by krauss
merged
2010-03-02, by haftmann
dropped superfluous naming
2010-03-02, by haftmann
UNIV is not a logical constant
2010-03-02, by huffman
merged
2010-03-02, by huffman
re-enable bisim code, now in domain_theorems.ML
2010-03-02, by huffman
add missing rule to case_strict proof script
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
domain package no longer generates copy functions; all proofs use take functions instead
2010-03-02, by huffman
need to explicitly include REP_convex
2010-03-01, by huffman
add lemma lub_eq
2010-03-01, by huffman
add lemmas about ssum_map and sprod_map
2010-03-01, by huffman
generate take_take rules
2010-03-01, by huffman
add function define_take_functions
2010-03-01, by huffman
add missing strictify rule to proof script
2010-03-01, by huffman
qualify constructor names with type name
2010-03-01, by huffman
move definition of case combinator to domain_constructors.ML
2010-03-01, by huffman
remove dependence on Domain_Library
2010-03-01, by huffman
more uses of function get_vars
2010-03-01, by huffman
add functions get_vars, get_vars_avoiding
2010-03-01, by huffman
move proofs of pat_rews to domain_constructors.ML
2010-03-01, by huffman
add_domain_constructors takes iso_info record as argument
2010-02-28, by huffman
domain_isomorphism package proves deflation rules for map functions
2010-02-28, by huffman
store deflation thms for map functions in theory data
2010-02-28, by huffman
use function list_ccomb
2010-02-28, by huffman
add function define_const
2010-02-28, by huffman
fix infix declarations
2010-02-28, by huffman
move common functions into new file holcf_library.ML
2010-02-28, by huffman
get rid of incomplete pattern match warnings
2010-02-28, by huffman
move some powerdomain stuff into a new file
2010-02-28, by huffman
move case combinator syntax to domain_constructors.ML
2010-02-28, by huffman
remove redundant code
2010-02-28, by huffman
use correct syntax name for pattern combinator
2010-02-28, by huffman
fix output translation for Case syntax
2010-02-28, by huffman
move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-28, by huffman
domain_isomorphism function returns iso_info record
2010-02-27, by huffman
move proofs of match_rews to domain_constructors.ML
2010-02-27, by huffman
remove dead code
2010-02-27, by huffman
removed dead code
2010-02-27, by huffman
register match functions from domain_constructors.ML
2010-02-27, by huffman
move definition of match combinators to domain_constructors.ML
2010-02-27, by huffman
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
2010-02-27, by huffman
move definition of discriminators to domain_constructors.ML
2010-02-27, by huffman
move proofs of when_rews intro domain_constructors.ML
2010-02-27, by huffman
moved proofs of dist_les and dist_eqs to domain_constructors.ML
2010-02-27, by huffman
move proofs of casedist into domain_constructors.ML
2010-02-27, by huffman
move proofs of injects and inverts to domain_constructors.ML
2010-02-26, by huffman
reuse vars_of function
2010-02-26, by huffman
remove unnecessary stuff from argument to add_constructors function
2010-02-26, by huffman
reorder sections
2010-02-26, by huffman
move proof of con_rews into domain_constructor.ML
2010-02-26, by huffman
don't bother returning con_defs
2010-02-26, by huffman
move constructor-specific stuff to a separate function
2010-02-26, by huffman
replace prove_thm function
2010-02-26, by huffman
move proof of compactness rules into domain_constructors.ML
2010-02-26, by huffman
add some convenience functions
2010-02-26, by huffman
rewrite domain package code for selector functions
2010-02-25, by huffman
add function beta_of_def
2010-02-24, by huffman
reorganizing domain package code (in progress)
2010-02-24, by huffman
change domain package's treatment of variable names in theorems to be like datatype package
2010-02-24, by huffman
remove redundant lemma real_minus_half_eq
2010-02-24, by huffman
polished and converted some proofs to Isar style
2010-02-24, by huffman
killed more recdefs
2010-03-02, by krauss
tuned comment
2010-03-01, by krauss
repaired subscripts broken in d8d7d1b785af
2010-03-02, by haftmann
repaired definition (cf. d8d7d1b785af)
2010-03-02, by haftmann
authentic syntax for *all* logical entities;
2010-03-03, by wenzelm
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
2010-03-03, by wenzelm
notation for xsymbols (cf. ad039d29e01c);
2010-03-03, by wenzelm
"_type_prop" is syntax const -- recovered printing of OFCLASS;
2010-03-03, by wenzelm
removed unused external_names;
2010-03-03, by wenzelm
cleanup type translations;
2010-03-03, by wenzelm
adapted to authentic syntax -- actual types are verbatim;
2010-03-03, by wenzelm
authentic syntax for classes and type constructors;
2010-03-03, by wenzelm
more systematic mark/unmark operations;
2010-03-03, by wenzelm
proper (type_)notation;
2010-03-02, by wenzelm
proper antiquotations;
2010-03-02, by wenzelm
standard convention for syntax consts;
2010-03-02, by wenzelm
more precise scope of exception handler;
2010-03-02, by wenzelm
eliminated hard tabs;
2010-03-01, by wenzelm
tuned final whitespace;
2010-03-01, by wenzelm
repaired 'definition' (cf. d8d7d1b785af);
2010-03-01, by wenzelm
merged
2010-03-01, by wenzelm
more recdef (and old primrec) hunting
2010-03-01, by krauss
killed recdefs in HOL-Auth
2010-03-01, by krauss
merged
2010-03-01, by haftmann
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-03-01, by haftmann
export add_quotient_type.
2010-03-01, by Cezary Kaliszyk
updated generated files;
2010-03-01, by wenzelm
added type_notation command;
2010-03-01, by wenzelm
more uniform treatment of syntax for types vs. consts;
2010-03-01, by wenzelm
made smlnj happy
2010-03-01, by bulwahn
more antiquotations;
2010-02-28, by wenzelm
more antiquotations;
2010-02-28, by wenzelm
modernized structure Term_Ord;
2010-02-27, by wenzelm
use existing Typ_Graph;
2010-02-27, by wenzelm
further standard instances of functor Graph;
2010-02-27, by wenzelm
code simplification by inlining;
2010-02-27, by wenzelm
just one copy of structure Term_Graph (in Pure);
2010-02-27, by wenzelm
modernized structure Int_Graph;
2010-02-27, by wenzelm
clarified @{const_name} vs. @{const_abbrev};
2010-02-27, by wenzelm
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
2010-02-27, by wenzelm
type/const name: explicitly allow abbreviations as well;
2010-02-27, by wenzelm
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-27, by wenzelm
added at-poly-test, which is intended for performance tests of Poly/ML itself;
2010-02-27, by wenzelm
more precise syntax antiquotations;
2010-02-27, by wenzelm
ML antiquotations for type classes;
2010-02-27, by wenzelm
read_class: perform actual read, with source position;
2010-02-27, by wenzelm
parallel brute-force disambiguation;
2010-02-27, by wenzelm
degrade gracefully in CRITICAL section;
2010-02-27, by wenzelm
gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;
2010-02-26, by wenzelm
tuned;
2010-02-26, by wenzelm
use simplified Syntax.escape;
2010-02-26, by wenzelm
tuned hyp_subst_tac';
2010-02-26, by wenzelm
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
2010-02-26, by blanchet
merged
2010-02-26, by blanchet
more work on the new monotonicity stuff in Nitpick
2010-02-26, by blanchet
improved precision of infinite "shallow" datatypes in Nitpick;
2010-02-25, by blanchet
cosmetics
2010-02-25, by blanchet
merged
2010-02-26, by bulwahn
merged
2010-02-26, by bulwahn
adding no_topmost_reordering as new option to the code_pred command
2010-02-25, by bulwahn
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
2010-02-25, by bulwahn
added quiet option to quickcheck command
2010-02-25, by bulwahn
added basic reporting of test cases to quickcheck
2010-02-25, by bulwahn
merged
2010-02-26, by haftmann
use abstract code cerficates for bare code theorems
2010-02-26, by haftmann
implement quotient_of for odl SML code generator
2010-02-26, by haftmann
adjusted to cs. e4a7947e02b8
2010-02-26, by haftmann
bound argument for abstype proposition
2010-02-24, by haftmann
renamed theory Rational to Rat
2010-02-24, by haftmann
tuned whitespace
2010-02-24, by haftmann
more precise exception handler
2010-02-24, by haftmann
more general case and induct rules; normalize and quotient_of; abstract code generation
2010-02-24, by haftmann
crossproduct coprimality lemmas
2010-02-24, by haftmann
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
2010-02-24, by haftmann
evaluation for abstypes
2010-02-24, by haftmann
modernized structure Split_Rule;
2010-02-25, by wenzelm
more antiquotations;
2010-02-25, by wenzelm
explicit @{type_syntax} markup;
2010-02-25, by wenzelm
explicit @{type_syntax} markup;
2010-02-25, by wenzelm
more orthogonal antiquotations for type constructors;
2010-02-25, by wenzelm
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-25, by wenzelm
provide direct access to the different kinds of type declarations;
2010-02-25, by wenzelm
use mixfix syntax for Boogie types
2010-02-25, by boehmes
merged
2010-02-24, by wenzelm
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
2010-02-24, by boehmes
modernized syntax declarations, and make them actually work with authentic syntax;
2010-02-24, by wenzelm
observe standard convention for syntax consts;
2010-02-24, by wenzelm
proper type syntax (cf. 7425aece4ee3);
2010-02-24, by wenzelm
observe standard convention for syntax consts;
2010-02-24, by wenzelm
allow general mixfix syntax for type constructors;
2010-02-24, by wenzelm
merged
2010-02-24, by huffman
merged
2010-02-23, by huffman
remove redundant lemma realpow_increasing
2010-02-23, by huffman
remove redundant simp rules from RealPow.thy
2010-02-23, by huffman
adapt to new realpow rules
2010-02-23, by huffman
adapt to changes in simpset
2010-02-23, by huffman
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
2010-02-23, by huffman
move float syntax from RealPow to Rational
2010-02-23, by huffman
compile
2010-02-24, by blanchet
merged
2010-02-24, by blanchet
compile
2010-02-24, by blanchet
make example compile
2010-02-24, by blanchet
got rid of "axclass", apparently
2010-02-24, by blanchet
merged
2010-02-24, by blanchet
cosmetics
2010-02-24, by blanchet
support local definitions in Nitpick
2010-02-23, by blanchet
show Kodkod warning message even in non-verbose mode
2010-02-23, by blanchet
distinguish between Kodkodi warnings and errors in Nitpick;
2010-02-23, by blanchet
optimized multisets in Nitpick by fishing "finite"
2010-02-23, by blanchet
document Quickcheck's "no_assms" option
2010-02-23, by blanchet
tuned comment
2010-02-24, by haftmann
merged
2010-02-23, by hoelzl
Moved old Integration to examples.
2010-02-23, by hoelzl
merged
2010-02-23, by bulwahn
merged
2010-02-23, by bulwahn
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
2010-02-23, by bulwahn
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-02-23, by bulwahn
separated narrowing timeouts for intermediate and final steps
2010-02-23, by boehmes
merged
2010-02-23, by haftmann
merged
2010-02-23, by haftmann
dropped axclass; dropped Id; session theory Hoare.thy
2010-02-23, by haftmann
dropped session W0; c.f. MiniML in AFP
2010-02-23, by haftmann
dropped axclass, going back to purely syntactic type classes
2010-02-23, by haftmann
dropped axclass; dropped Id
2010-02-23, by haftmann
dropped axclass; dropped Id; session theory Hoare.thy
2010-02-23, by haftmann
dropped axclass
2010-02-23, by haftmann
export prs_rules and rsp_rules attributes
2010-02-23, by Cezary Kaliszyk
merge
2010-02-23, by blanchet
improved precision of small sets in Nitpick
2010-02-23, by blanchet
improved Nitpick's support for quotient types
2010-02-23, by blanchet
Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration
2010-02-23, by hoelzl
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
2010-02-23, by blanchet
mind the "s"
2010-02-23, by haftmann
merged
2010-02-23, by haftmann
NEWS
2010-02-22, by haftmann
added missing separator
2010-02-22, by haftmann
more accurate when registering new types
2010-02-22, by haftmann
added Dlist
2010-02-22, by haftmann
tuned text
2010-02-22, by haftmann
distributed theory Algebras to theories Groups and Lattices
2010-02-22, by haftmann
merged
2010-02-22, by haftmann
proper distinction of code datatypes and abstypes
2010-02-22, by haftmann
merged
2010-02-22, by haftmann
merged
2010-02-22, by haftmann
merged
2010-02-22, by haftmann
lemma distinct_insert
2010-02-20, by haftmann
proper header and subsection headings
2010-02-22, by huffman
remove unneeded premise from rat_floor_lemma and floor_Fract
2010-02-22, by huffman
Replaced Integration by Multivariate-Analysis/Real_Integration
2010-02-22, by hoelzl
Support for one-dimensional integration in Multivariate-Analysis
2010-02-22, by himmelma
Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
2010-02-18, by himmelma
merged
2010-02-22, by huffman
add mixfix field to type Domain_Library.cons
2010-02-22, by huffman
remove unnecessary local
2010-02-22, by huffman
update to use fixrec package
2010-02-21, by huffman
merge
2010-02-22, by blanchet
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-22, by blanchet
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
2010-02-22, by blanchet
dropped references to old axclass from documentation
2010-02-22, by haftmann
Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
2010-02-22, by berghofe
fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-22, by blanchet
update the keywords files
2010-02-22, by Cezary Kaliszyk
rename print_maps to print_quotmaps
2010-02-22, by Cezary Kaliszyk
adjusted to cs. 8dfd816713c6
2010-02-22, by haftmann
NEWS
2010-02-22, by haftmann
merged
2010-02-22, by haftmann
tuned proofs
2010-02-22, by haftmann
ascii syntax for multiset order
2010-02-22, by haftmann
switched notations for pointwise and multiset order
2010-02-22, by haftmann
NEWS
2010-02-22, by haftmann
NEWS
2010-02-19, by haftmann
merged
2010-02-19, by haftmann
switched notations for pointwise and multiset order
2010-02-19, by haftmann
moved remaning class operations from Algebras.thy to Groups.thy
2010-02-19, by haftmann
hide fact range_def
2010-02-19, by haftmann
dropped reference to type classes
2010-02-19, by haftmann
NEWS
2010-02-19, by haftmann
filter out authentic const syntax;
2010-02-21, by wenzelm
slightly more abstract syntax mark/unmark operations;
2010-02-21, by wenzelm
tuned;
2010-02-21, by wenzelm
NEWS: authentic syntax for *all* term constants;
2010-02-21, by wenzelm
concrete syntax for all constructors, to workaround authentic syntax problem with domain package;
2010-02-21, by wenzelm
adapted to authentic syntax;
2010-02-21, by wenzelm
adapted to authentic syntax;
2010-02-21, by wenzelm
adapted to authentic syntax;
2010-02-21, by wenzelm
authentic syntax for *all* term constants;
2010-02-21, by wenzelm
binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
2010-02-21, by wenzelm
tuned headers;
2010-02-21, by wenzelm
simplified syntax -- to make it work for authentic syntax;
2010-02-21, by wenzelm
modernized notation -- to make it work for authentic syntax;
2010-02-21, by wenzelm
proper markup of const syntax;
2010-02-21, by wenzelm
more precise dependencies;
2010-02-20, by wenzelm
added lemma
2010-02-20, by nipkow
moved reduced Induct/SList back from AFP.
2010-02-20, by nipkow
adjusted to changes in cs b987b803616d
2010-02-20, by haftmann
disabled some old (fragile) isatests;
2010-02-19, by wenzelm
tuned settings;
2010-02-19, by wenzelm
fixed document;
2010-02-19, by wenzelm
eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;
2010-02-19, by wenzelm
made SML/NJ happy;
2010-02-19, by wenzelm
tuned;
2010-02-19, by wenzelm
authentic term syntax;
2010-02-19, by wenzelm
Thm.def_binding;
2010-02-19, by wenzelm
moved ancient Drule.get_def to OldGoals.get_def;
2010-02-19, by wenzelm
quote the constant and theorem name with @{text}
2010-02-19, by Cezary Kaliszyk
merged
2010-02-19, by wenzelm
merged
2010-02-19, by wenzelm
local Simplifier.context;
2010-02-19, by wenzelm
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19, by wenzelm
tuned message;
2010-02-19, by wenzelm
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-02-19, by wenzelm
merged
2010-02-19, by haftmann
context theorem is optional
2010-02-19, by haftmann
added dest_comb
2010-02-19, by haftmann
a simple concept for datatype invariants
2010-02-19, by haftmann
using Code.bare_thms_of_cert
2010-02-19, by haftmann
simplified
2010-02-19, by haftmann
added code_abstype keyword
2010-02-19, by haftmann
Initial version of HOL quotient package.
2010-02-19, by Cezary Kaliszyk
merge
2010-02-19, by blanchet
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-18, by blanchet
fix bug in Nitpick's monotonicity code w.r.t. binary integers
2010-02-18, by blanchet
merged
2010-02-18, by wenzelm
merged
2010-02-18, by huffman
get rid of many duplicate simp rule warnings
2010-02-18, by huffman
get rid of warnings about duplicate simp rules in all HOLCF theories
2010-02-18, by huffman
HOLCF-FOCUS depends on ex/Stream.thy
2010-02-18, by huffman
fix looping call to simplifier
2010-02-18, by huffman
merged
2010-02-18, by berghofe
Use top-down rewriting to contract abbreviations.
2010-02-18, by berghofe
Added function rewrite_term_top for top-down rewriting.
2010-02-18, by berghofe
merged
2010-02-18, by nipkow
added lemma
2010-02-18, by nipkow
merged
2010-02-18, by wenzelm
tuned isatest settings;
2010-02-18, by wenzelm
removed unused Theory_Target.begin;
2010-02-18, by wenzelm
locale: more precise treatment of naming vs. binding;
2010-02-18, by wenzelm
Sign.restore_naming -- slightly more robust;
2010-02-18, by wenzelm
typedef: slightly more precise treatment of binding;
2010-02-18, by wenzelm
axclass: more precise treatment of naming vs. binding;
2010-02-18, by wenzelm
more systematic treatment of qualified names derived from binding;
2010-02-18, by wenzelm
pretty_full_theory: proper Syntax.init_pretty_global;
2010-02-18, by wenzelm
made SML/NJ happy (again);
2010-02-18, by wenzelm
merged
2010-02-18, by haftmann
drop code lemma for ordered_keys
2010-02-18, by haftmann
more lemmas about sort(_key)
2010-02-17, by haftmann
added ordered_keys
2010-02-17, by haftmann
isatest: activated HOL-Nitpick_Examples for x86_64-darwin -- should now work with kodkodi-1.2.8;
2010-02-17, by wenzelm
merged
2010-02-17, by blanchet
fix example to reflect change in function signature
2010-02-17, by blanchet
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17, by blanchet
added gotcha to Nitpick manual regarding nonstandard models of "nat"
2010-02-17, by blanchet
improve Nitpick's "Datatypes" rendering for elements containing cycles
2010-02-17, by blanchet
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
2010-02-17, by blanchet
merged
2010-02-17, by blanchet
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-17, by blanchet
merge
2010-02-17, by blanchet
reintroduce structural induction hint in Nitpick
2010-02-17, by blanchet
merge
2010-02-17, by blanchet
synchronize Nitpick's wellfoundedness formulas caching
2010-02-17, by blanchet
more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-13, by blanchet
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-13, by blanchet
minor fixes to Nitpick
2010-02-12, by blanchet
various cosmetic changes to Nitpick
2010-02-12, by blanchet
merged
2010-02-17, by huffman
fix more looping simp rules
2010-02-17, by huffman
remove $ from all HOLCF files
2010-02-17, by huffman
Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration.
2010-02-17, by hoelzl
Added integration to Multivariate-Analysis (upto FTC)
2010-02-17, by himmelma
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
2010-02-17, by hoelzl
fix looping simp rule
2010-02-17, by huffman
fix warnings about duplicate simp rules
2010-02-17, by huffman
fix warnings about duplicate simp rules
2010-02-17, by huffman
add theory HOLCF/ex/Strict_Fun.thy
2010-02-17, by huffman
tuned primrec signature: return definienda
2010-02-17, by haftmann
merged
2010-02-17, by haftmann
example for executable choice
2010-02-17, by haftmann
added simple theory about discrete summation
2010-02-17, by haftmann
giving up sunbroy2;
2010-02-17, by wenzelm
merged
2010-02-17, by haftmann
a draft for an example how to turn specifications involving choice executable
2010-02-17, by haftmann
added lemma map_of_map_restrict; generalized lemma dom_const
2010-02-17, by haftmann
adjusted to changes in theory Mapping
2010-02-17, by haftmann
more close integration with theory Map
2010-02-17, by haftmann
mappings implemented by association lists
2010-02-17, by haftmann
merged
2010-02-16, by wenzelm
updated SMT certificates
2010-02-16, by boehmes
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
2010-02-16, by boehmes
updated SMT certificates
2010-02-16, by boehmes
added Cache_IO: cache for output of external tools,
2010-02-16, by boehmes
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
2010-02-16, by hoelzl
simplified/clarified record print translations;
2010-02-16, by wenzelm
eliminated camel case;
2010-02-16, by wenzelm
tuned;
2010-02-16, by wenzelm
simplified/clarified record translations;
2010-02-16, by wenzelm
moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-16, by wenzelm
tuned;
2010-02-16, by wenzelm
comment;
2010-02-16, by wenzelm
conceal internal record definitions;
2010-02-16, by wenzelm
simplified meaning of ProofContext.verbose;
2010-02-16, by wenzelm
refrain from using @{const_name} in syntax translations;
2010-02-16, by wenzelm
misc tuning and simplification;
2010-02-16, by wenzelm
refined and exported record_info;
2010-02-15, by wenzelm
modernized structures;
2010-02-15, by wenzelm
modernized signature -- proper binding;
2010-02-15, by wenzelm
tuned errors;
2010-02-15, by wenzelm
Typedef.the_info;
2010-02-15, by wenzelm
formal markup of constants;
2010-02-15, by wenzelm
tuned document;
2010-02-15, by wenzelm
eliminated old fold;
2010-02-15, by wenzelm
renamed InfixName to Infix etc.;
2010-02-15, by wenzelm
discontinued unnamed infix syntax;
2010-02-15, by wenzelm
eliminated unnamed infixes;
2010-02-15, by wenzelm
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
2010-02-15, by haftmann
clarifed type
2010-02-15, by haftmann
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
2010-02-14, by boehmes
formal markup of constants;
2010-02-14, by wenzelm
modernized structures;
2010-02-13, by wenzelm
authentic proof syntax;
2010-02-13, by wenzelm
tuned import order
2010-02-12, by haftmann
tuned comments
2010-02-12, by haftmann
merged
2010-02-11, by wenzelm
merged
2010-02-11, by huffman
change generated lemmas dist_eqs and dist_les to iff-style
2010-02-11, by huffman
unfold quantifiers (Ball, Bex, Ex1)
2010-02-11, by boehmes
modernized translations;
2010-02-11, by wenzelm
formal markup of @{syntax_const} and @{const_syntax};
2010-02-11, by wenzelm
modernized translations;
2010-02-11, by wenzelm
numeral syntax: clarify parse trees vs. actual terms;
2010-02-11, by wenzelm
added ML antiquotation @{syntax_const};
2010-02-11, by wenzelm
treat inner token markers as syntax consts;
2010-02-11, by wenzelm
modernized syntax/translations;
2010-02-11, by wenzelm
modernized syntax/translations;
2010-02-11, by wenzelm
modernized translations;
2010-02-11, by wenzelm
merged
2010-02-11, by boehmes
use full paths when importing theories
2010-02-11, by boehmes
merged
2010-02-11, by nipkow
inductive vs inductive_set explanation
2010-02-11, by nipkow
modernized translations;
2010-02-11, by wenzelm
modernized translations;
2010-02-10, by wenzelm
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10, by wenzelm
merged
2010-02-10, by berghofe
Fixed bug in code for guessing the name of the variable representing the freshness context.
2010-02-10, by berghofe
dropped last occurence of the linlinordered accident
2010-02-10, by haftmann
dropped Id
2010-02-10, by haftmann
minor metis proof tuning
2010-02-10, by haftmann
merged
2010-02-10, by haftmann
NEWS
2010-02-10, by haftmann
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10, by haftmann
revert uninspired Structure_Syntax experiment
2010-02-10, by haftmann
moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-10, by haftmann
merged
2010-02-10, by wenzelm
unset KODKODI explicitly -- apparently isatest patches settings cumulatively;
2010-02-10, by wenzelm
make Nitpick test a bit weaker;
2010-02-10, by blanchet
merged
2010-02-10, by haftmann
moved constants inverse and divide to Ring.thy
2010-02-10, by haftmann
moved constants inverse and divide to Ring.thy
2010-02-10, by haftmann
division ring assumes divide_inverse
2010-02-10, by haftmann
rely less on ordered rewriting
2010-02-10, by haftmann
merged
2010-02-10, by wenzelm
merged
2010-02-09, by blanchet
merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-09, by blanchet
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
2010-02-09, by blanchet
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
2010-02-09, by blanchet
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
2010-02-05, by blanchet
handle Nitpick's nonstandard model enumeration in a cleaner way;
2010-02-05, by blanchet
proper quoting of file paths when invoking Kodkodi from Nitpick
2010-02-05, by blanchet
merged
2010-02-05, by blanchet
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
2010-02-05, by blanchet
adapted example following previous Nitpick change and fixed minor optimization in Nitpick
2010-02-04, by blanchet
split "nitpick_hol.ML" into two files to make it more manageable;
2010-02-04, by blanchet
removed obsolete CVS Ids;
2010-02-10, by wenzelm
modernized translations;
2010-02-10, by wenzelm
modernized syntax translations, using mostly abbreviation/notation;
2010-02-10, by wenzelm
simple proofs make life faster and easier
2010-02-09, by haftmann
merged
2010-02-09, by haftmann
hide fact names clashing with fact names from Group.thy
2010-02-09, by haftmann
dropped lemma duplicates
2010-02-09, by haftmann
isatest: activated HOL-Nitpick_Examples (by adding component kodkodi) on some platforms where it mostly works as expected;
2010-02-09, by wenzelm
adjusted to cs. 9f841f20dca6
2010-02-09, by haftmann
merged
2010-02-08, by huffman
correct definedness side conditions for copy_apps and take_apps
2010-02-08, by huffman
handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
2010-02-08, by huffman
rewrite proof script for take_stricts
2010-02-07, by huffman
remove redundant theorem attributes
2010-02-07, by huffman
add lemma iterate_below_fix
2010-02-07, by huffman
modernized some syntax translations;
2010-02-08, by wenzelm
more precise dependencies;
2010-02-08, by wenzelm
merged
2010-02-08, by haftmann
re-generated certificates
2010-02-08, by haftmann
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08, by haftmann
tuned spelling
2010-02-08, by haftmann
tuned proofs
2010-02-08, by haftmann
hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-02-08, by haftmann
tuned header
2010-02-08, by haftmann
using code antiquotation
2010-02-08, by haftmann
tuned header
2010-02-08, by haftmann
dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08, by haftmann
NEWS: ax_simps
2010-02-08, by haftmann
avoid upto in generated code (is infix operator in library.ML)
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
2010-02-08, by haftmann
merged
2010-02-08, by haftmann
more precise proofs
2010-02-08, by haftmann
moved auxiliary lemmas to more appropriate places
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
2010-02-08, by haftmann
dropped instantiations for combined lattices
2010-02-08, by haftmann
added lemmas involving Min, Max, uminus
2010-02-08, by haftmann
tuned proof
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures
2010-02-08, by haftmann
more quotes;
2010-02-08, by wenzelm
merged
2010-02-08, by haftmann
separate theory for index structures
2010-02-08, by haftmann
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05, by haftmann
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05, by haftmann
added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration
2010-02-05, by haftmann
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
2010-02-08, by boehmes
removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);
2010-02-07, by wenzelm
modernized perl scripts: prefer standalone executables;
2010-02-07, by wenzelm
modernized perl scripts: prefer standalone executables;
2010-02-07, by wenzelm
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-07, by wenzelm
prefer explicit @{lemma} over adhoc forward reasoning;
2010-02-07, by wenzelm
simplified interface for ML antiquotations, struct_name is always "Isabelle";
2010-02-07, by wenzelm
tuned isatest ML_OPTIONS;
2010-02-06, by wenzelm
removed ever experimental support for Moscow ML -- hardly works anymore;
2010-02-06, by wenzelm
result: Single_Assignment.var;
2010-02-06, by wenzelm
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
2010-02-06, by wenzelm
explicit representation of single-assignment variables;
2010-02-06, by wenzelm
fixed spelling;
2010-02-06, by wenzelm
removed unused "boundary" of Table/Graph.get_first;
2010-02-06, by wenzelm
proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
2010-02-06, by wenzelm
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2010-02-06, by wenzelm
misc tuning;
2010-02-06, by wenzelm
merged
2010-02-06, by haftmann
adjusted to changeset 118b41bba42b5
2010-02-06, by haftmann
tuned font handling;
2010-02-06, by wenzelm
updated versions of requirements;
2010-02-05, by wenzelm
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
2010-02-05, by wenzelm
eliminated self intersection and non-integer coordinates;
2010-02-05, by wenzelm
try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
2010-02-05, by wenzelm
updated generated files;
2010-02-05, by wenzelm
merged
2010-02-05, by wenzelm
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
2010-02-04, by hoelzl
four changes to Nitpick:
2010-02-04, by blanchet
capture error messages (of SMT solvers)
2010-02-02, by boehmes
updated dependencies
2010-02-02, by boehmes
merged
2010-02-02, by boehmes
updated SMT certificates
2010-02-02, by boehmes
updated examples due to changes in the way SMT certificates are stored
2010-02-02, by boehmes
merged
2010-02-02, by berghofe
merged
2010-01-31, by berghofe
Adapted to changes in cases method.
2010-01-30, by berghofe
Adapted to changes in setup of cases method.
2010-01-30, by berghofe
Added setup for simplification of equality constraints in cases rules.
2010-01-30, by berghofe
Added infrastructure for simplifying equality constraints in cases rules.
2010-01-30, by berghofe
Added "constraints" tag / attribute for specifying the number of equality
2010-01-30, by berghofe
updated SMT certificates
2010-02-02, by boehmes
updated SMT examples
2010-02-02, by boehmes
collect certificates in a single file
2010-02-02, by boehmes
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-02-02, by blanchet
Removed explicit type annotations
2010-02-01, by himmelma
adjusted to changes in List_Set.thy
2010-01-31, by haftmann
more correspondence lemmas between related operations
2010-01-31, by haftmann
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
dropped some redundancies
2010-01-31, by haftmann
generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
more correspondence lemmas between related operations; tuned some proofs
2010-01-31, by haftmann
new theory Algebras.thy for generic algebraic structures
2010-01-28, by haftmann
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-28, by haftmann
merged
2010-01-27, by haftmann
a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
2010-01-27, by haftmann
lemma Image_closed_trancl
2010-01-27, by haftmann
corrected type of typecopy constructor
2010-01-27, by haftmann
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
2010-01-27, by haftmann
Changed author; removed debugging code.
2010-01-27, by berghofe
merged
2010-01-25, by bulwahn
adding Mutabelle to repository
2010-01-25, by bulwahn
Replaced vec1 and dest_vec1 by abbreviation.
2010-01-25, by hoelzl
merged
2010-01-22, by haftmann
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22, by haftmann
merged
2010-01-22, by boehmes
support skolem constant for extensional arrays in Z3 proofs
2010-01-22, by boehmes
drop underscores at end of names coming from Boogie
2010-01-22, by boehmes
merged
2010-01-22, by bulwahn
correctly hiding facts of Lazy_Sequence
2010-01-22, by bulwahn
corrected and simplified Spec_Rules registration in the Recdef package
2010-01-21, by bulwahn
merged
2010-01-21, by bulwahn
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
2010-01-21, by bulwahn
adopting Sequences
2010-01-20, by bulwahn
added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2010-01-20, by bulwahn
merged
2010-01-20, by bulwahn
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-18, by krauss
merged
2010-01-20, by bulwahn
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-20, by bulwahn
simplified proofs
2010-01-22, by haftmann
NEWS
2010-01-22, by haftmann
more accurate dependencies
2010-01-22, by haftmann
code literals: distinguish numeral classes by different entries
2010-01-22, by haftmann
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
2010-01-22, by haftmann
merged
2010-01-21, by haftmann
dropped some old primrecs and some constdefs
2010-01-16, by haftmann
explicit CONST in translations
2010-01-16, by haftmann
modernized syntax
2010-01-16, by haftmann
fix issues with previous Nitpick change
2010-01-20, by blanchet
merged
2010-01-20, by blanchet
some work on Nitpick's support for quotient types;
2010-01-20, by blanchet
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
2010-01-14, by blanchet
Added transpose_rectangle, when the input list is rectangular.
2010-01-19, by hoelzl
Add transpose to the List-theory.
2010-01-19, by hoelzl
some examples for basic context operations;
2010-02-02, by wenzelm
minimal tuning of this slightly dated material;
2010-02-02, by wenzelm
added Subgoal.FOCUS;
2010-02-02, by wenzelm
misc tuning and clarification;
2010-02-02, by wenzelm
moved examples to proper place;
2010-02-02, by wenzelm
more details on long names, binding/naming, name space;
2010-02-01, by wenzelm
Variable.names_of;
2010-01-31, by wenzelm
more details on Isabelle symbols;
2010-01-31, by wenzelm
theory data example;
2010-01-29, by wenzelm
basic setup for ML examples: tag "mlex";
2010-01-29, by wenzelm
tuned signature;
2010-01-28, by wenzelm
formal markup of type aliases;
2010-01-28, by wenzelm
make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
2010-01-28, by wenzelm
Netbeans Library "Scala-compiler";
2010-01-16, by wenzelm
union is an abbreviation for sup.
2010-01-15, by berghofe
merged
2010-01-15, by berghofe
Eliminated is_open option of Rule_Cases.make_nested/make_common;
2010-01-15, by berghofe
Adapted to changes in induct method.
2010-01-10, by berghofe
Adapted to changes in setup of induct method.
2010-01-10, by berghofe
Expand proofs of induct_atomize'/rulify'.
2010-01-10, by berghofe
Changed case names of converse_rtranclp_induct.
2010-01-10, by berghofe
Injectivity / distinctness theorems are now used to simplify induction rules.
2010-01-10, by berghofe
same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-10, by berghofe
Tuned some proofs; nicer case names for some of the induction / cases rules.
2010-01-10, by berghofe
Added setup for simplification of equality constraints in induction rules.
2010-01-10, by berghofe
Added infrastructure for simplifying equality constraints.
2010-01-10, by berghofe
spurious proof failure
2010-01-15, by haftmann
merged
2010-01-14, by haftmann
merged
2010-01-14, by haftmann
dropped unused binding
2010-01-14, by haftmann
dedicated conversions to and from Int
2010-01-14, by haftmann
printing of cases
2010-01-14, by haftmann
tuned for products vs. tupled functions
2010-01-14, by haftmann
added Scala setup
2010-01-14, by haftmann
allow individual printing of numerals during code serialization
2010-01-14, by haftmann
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2010-01-14, by blanchet
adjusted to changes in code equation administration
2010-01-14, by haftmann
explicit abstract type of code certificates
2010-01-13, by haftmann
corrected error messages; tuned
2010-01-13, by haftmann
function transformer preprocessor applies to both code generators
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
code certificates as integral part of code generation
2010-01-12, by haftmann
import of antiquote_setup not necessary
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
being more accurate wrt. list syntax
2010-01-13, by haftmann
deactivate pretty code test for Scala -- no proper setup yet
2010-01-13, by haftmann
some syntax setup for Scala
2010-01-13, by haftmann
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2010-01-13, by wenzelm
merged
2010-01-12, by wenzelm
Parsing errors during proof reconstruction now give rise to an intelligible error message.
2010-01-12, by paulson
rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
2010-01-12, by wenzelm
tuned initial properties/perspective;
2010-01-12, by wenzelm
provide JEDIT_SETTINGS via settings;
2010-01-12, by wenzelm
updated version and dependencies;
2010-01-12, by wenzelm
recovered subscript (cf. ded5b770ec1c);
2010-01-12, by wenzelm
formal antiquotations for ML snippets; no "open" unsynchronized references
2010-01-12, by haftmann
clarified terminology;
2010-01-11, by wenzelm
merged
2010-01-11, by wenzelm
added code certificates
2010-01-11, by haftmann
tuned code equations
2010-01-11, by haftmann
Matrices form a semiring with 0
2010-01-11, by hoelzl
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
2010-01-11, by wenzelm
ignore some src/Tools/jEdit stuff;
2010-01-11, by wenzelm
merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b
2010-01-11, by wenzelm
more timing;
2010-01-11, by wenzelm
more tobust treatment of Document.current_state;
2010-01-11, by wenzelm
new unparsed span for text right after existing command;
2010-01-11, by wenzelm
Outer_Lex.is_ignored;
2010-01-11, by wenzelm
simplified Text_Edit;
2010-01-11, by wenzelm
eliminated strange mutable var commands;
2010-01-11, by wenzelm
updated header;
2010-01-11, by wenzelm
eliminated obsolete isabelle.proofdocument.Token;
2010-01-11, by wenzelm
do not override Command.hashCode -- which was inconsistent with eq anyway;
2010-01-11, by wenzelm
renamed Command.content to source;
2010-01-11, by wenzelm
further tuning of command_start;
2010-01-10, by wenzelm
refrain from poking blink rate -- might get stuck in invisible state;
2010-01-10, by wenzelm
eliminated Command.stop, which tends to case duplicate traversal of commands;
2010-01-10, by wenzelm
iterators for ranges of commands/starts -- avoid extra array per document;
2010-01-10, by wenzelm
tuned document changes;
2010-01-10, by wenzelm
misc tuning and clarification of Document/Change;
2010-01-10, by wenzelm
adhoc reset of blink rate;
2010-01-10, by wenzelm
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
2010-01-10, by wenzelm
redirect scala.Console output during interpretation;
2010-01-09, by wenzelm
bind "session";
2010-01-09, by wenzelm
export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;
2010-01-09, by wenzelm
removed unused var plugin;
2010-01-09, by wenzelm
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
2010-01-09, by wenzelm
provide some bindings of jEdit values;
2010-01-09, by wenzelm
more precise prompt etc.;
2010-01-08, by wenzelm
define scala.home, for more robust startup of Scala tools, notably the compiler;
2010-01-08, by wenzelm
added jEdit Console and Scala compiler;
2010-01-08, by wenzelm
some attempts at Scala console plugin;
2010-01-08, by wenzelm
more precise treatment of document/state assigment;
2010-01-06, by wenzelm
more precise notion of bad messages;
2010-01-05, by wenzelm
use Text_Edit provided by Isabelle;
2010-01-05, by wenzelm
result.is_ready is not bad;
2010-01-05, by wenzelm
singleton status messages, with more precise patterns -- report bad messages;
2010-01-04, by wenzelm
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
2010-01-04, by wenzelm
slightly more uniform/robust handling of visible document;
2010-01-04, by wenzelm
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
2010-01-03, by wenzelm
more explicit treatment of command/document state;
2010-01-03, by wenzelm
removed unused document_change bus;
2010-01-03, by wenzelm
tuned;
2010-01-01, by wenzelm
tuned;
2010-01-01, by wenzelm
misc tuning;
2010-01-01, by wenzelm
tuned Change: eliminated redundant copy of document id;
2010-01-01, by wenzelm
eliminated redundant session documents database;
2010-01-01, by wenzelm
use isabelle.Future;
2010-01-01, by wenzelm
renamed current_document to recent_document (might be a bit older than current_change);
2010-01-01, by wenzelm
renamed Proof_Document to Document;
2010-01-01, by wenzelm
tuned dialog;
2009-12-31, by wenzelm
improved dialog;
2009-12-31, by wenzelm
basic setup for synchronous / modal (!) prover startup;
2009-12-31, by wenzelm
tuned signature;
2009-12-30, by wenzelm
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
2009-12-30, by wenzelm
tuned signature of isabelle.Position;
2009-12-30, by wenzelm
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
2009-12-30, by wenzelm
unified Command and Command_State, eliminated separate Accumulator;
2009-12-30, by wenzelm
removed experimental history panel;
2009-12-30, by wenzelm
more explicit modeling of Command and Command_State as Session.Entity;
2009-12-30, by wenzelm
updated;
2009-12-30, by wenzelm
tuned;
2009-12-29, by wenzelm
tuned caret_listener/selected_command;
2009-12-29, by wenzelm
misc tuning;
2009-12-29, by wenzelm
eliminated global Session.document_0 -- did not work due to hardwired id;
2009-12-29, by wenzelm
tuned;
2009-12-29, by wenzelm
tuned;
2009-12-29, by wenzelm
Standard_System;
2009-12-28, by wenzelm
slightly larger stack size -- default seems to be as low as 256k;
2009-12-23, by wenzelm
back to activate=startup (again) -- ensure that Isabelle_Encoding refers to valid Isabelle.system;
2009-12-23, by wenzelm
adapted to class Outer_Syntax;
2009-12-22, by wenzelm
renamed session.info to session.root;
2009-12-22, by wenzelm
tuned;
2009-12-22, by wenzelm
just one variable for outer syntax keywords and completion;
2009-12-22, by wenzelm
added isabelle-session mode for session.info files;
2009-12-21, by wenzelm
tuned keywords;
2009-12-21, by wenzelm
sort completions by plain string order;
2009-12-21, by wenzelm
cache results;
2009-12-18, by wenzelm
imitate PG 4 colors;
2009-12-18, by wenzelm
tuned;
2009-12-18, by wenzelm
simplified Isabelle_Process.Result;
2009-12-17, by wenzelm
explicit object Session.Global_Settings;
2009-12-16, by wenzelm
actually use JEDIT_JAVA_OPTIONS from settings, not ..._ARGS;
2009-12-16, by wenzelm
some explicit Swing_Thread guards;
2009-12-15, by wenzelm
direct apply for Document_Model and Document_View;
2009-12-15, by wenzelm
need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED;
2009-12-15, by wenzelm
merged
2009-12-15, by wenzelm
Cobra version;
2009-12-15, by wenzelm
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
2009-12-15, by wenzelm
clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
2009-12-15, by wenzelm
refined treatment of default logic concerning property and GUI;
2009-12-15, by wenzelm
handle "default" logic;
2009-12-11, by wenzelm
more serious command line handling;
2009-12-11, by wenzelm
proper uninstall;
2009-12-11, by wenzelm
removed unused Session.prover_logic;
2009-12-11, by wenzelm
class Session models full session, with or without prover process (cf. heaps, browser_info);
2009-12-10, by wenzelm
tuned;
2009-12-10, by wenzelm
basic setup for HTML_Panel event handling;
2009-12-10, by wenzelm
install_fonts;
2009-12-10, by wenzelm
renamed "raw output" to "protocol";
2009-12-08, by wenzelm
proper actor wiring for raw process output;
2009-12-08, by wenzelm
misc tuning;
2009-12-08, by wenzelm
prefer options from running application;
2009-12-08, by wenzelm
more precise messages;
2009-12-08, by wenzelm
back to low-level JPanel, required for addNotify/removeNotify;
2009-12-08, by wenzelm
added properties_changed event bus;
2009-12-08, by wenzelm
provide dummy URL;
2009-12-08, by wenzelm
generic HTML_Panel -- specific Results_Dockable;
2009-12-08, by wenzelm
tuned;
2009-12-08, by wenzelm
tuned;
2009-12-08, by wenzelm
simplified register_fonts;
2009-12-08, by wenzelm
tuned library names;
2009-12-08, by wenzelm
misc modernization of names;
2009-12-08, by wenzelm
misc rearrangement of files;
2009-12-08, by wenzelm
removed remains of Flying Saucer;
2009-12-08, by wenzelm
manipulate document within Swing thread only -- potentially slow;
2009-12-08, by wenzelm
tuned JVM settings;
2009-12-08, by wenzelm
misc updates;
2009-12-07, by wenzelm
obsolete;
2009-12-07, by wenzelm
use IsabelleText by default;
2009-12-07, by wenzelm
misc updates;
2009-12-07, by wenzelm
simplified treatment of Isabelle fonts, via Isabelle_System.register_fonts (requires Java 1.6);
2009-12-07, by wenzelm
removed ScrollerDockable, which is based on discontinued Flying Saucer renderer;
2009-12-07, by wenzelm
use IsabelleText font;
2009-12-07, by wenzelm
reduced logging;
2009-12-06, by wenzelm
tuned message markup;
2009-12-04, by wenzelm
plain results, no markup here;
2009-12-04, by wenzelm
basic setup for Cobra HTML renderer;
2009-12-04, by wenzelm
results: XML.Tree;
2009-12-04, by wenzelm
basic platform update;
2009-11-14, by wenzelm
Prover: private Actor;
2009-09-17, by wenzelm
tuned;
2009-09-16, by wenzelm
misc tuning;
2009-09-16, by wenzelm
Linear_Set.append_after;
2009-09-16, by wenzelm
tuned file name;
2009-09-15, by wenzelm
tuned file name;
2009-09-15, by wenzelm
renamed PhaseOverviewPanel to Document_Overview;
2009-09-15, by wenzelm
tooltip: HTML dummy;
2009-09-15, by wenzelm
tuned;
2009-09-15, by wenzelm
misc tuning and unification;
2009-09-15, by wenzelm
refrain from actor shutdown -- slightly low-level;
2009-09-15, by wenzelm
keep BufferListener and TextAreaExtension private;
2009-09-15, by wenzelm
tuned white space;
2009-09-15, by wenzelm
misc tuning;
2009-09-15, by wenzelm
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
2009-09-15, by wenzelm
single instance of rule_set;
2009-09-15, by wenzelm
regular activate=defer -- may debug remotely, no need to run under netbeans;
2009-09-13, by wenzelm
avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;
2009-09-13, by wenzelm
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
2009-09-08, by wenzelm
tuned;
2009-09-07, by wenzelm
tuned;
2009-09-07, by wenzelm
Prover: just one actor -- single message dispatch;
2009-09-07, by wenzelm
modernized Event_Bus -- based on actors;
2009-09-07, by wenzelm
eliminated ProverEvents.Activate -- handle "ready" within Prover;
2009-09-07, by wenzelm
corrected order
2009-09-07, by immler
sidekick root data: set buffer length to avoid crash of initial caret move;
2009-09-06, by wenzelm
tuned color (PG 4.0);
2009-09-06, by wenzelm
treat all messages except status as results;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
replaced find_command_at by command_at -- null-free, proper Option;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
tuned;
2009-09-06, by wenzelm
minor tuning;
2009-09-06, by wenzelm
tuned MarkupNode argument order;
2009-09-05, by wenzelm
eliminated MarkupInfo, moved particular variants into object Command;
2009-09-05, by wenzelm
removed dead code;
2009-09-05, by wenzelm
MarkupNode: removed id;
2009-09-05, by wenzelm
simplified MarkupNode -- independent of Command and ProofDocument;
2009-09-04, by wenzelm
minor tuning;
2009-09-04, by wenzelm
sorted;
2009-09-03, by wenzelm
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
2009-09-03, by wenzelm
tuned imports;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
State: immutable;
2009-09-03, by wenzelm
tuned;
2009-09-03, by wenzelm
minor tuning;
2009-09-03, by wenzelm
unified Swing_Thread.delay_first/last;
2009-09-02, by wenzelm
sealed Edit;
2009-09-02, by wenzelm
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
2009-09-01, by wenzelm
option -d: enable debugger;
2009-09-01, by wenzelm
modernized Isar_Document;
2009-09-01, by wenzelm
use Linear_Set from Isabelle/Pure.jar;
2009-09-01, by wenzelm
lazy fields
2009-08-27, by immler
better performance
2009-08-27, by immler
no busy waiting
2009-08-27, by immler
global event buses for changes concerning commands and document edits
2009-08-27, by immler
include scala-swing
2009-08-27, by immler
merged
2009-08-27, by immler
must unapply edits in reverse order
2009-08-27, by immler
fixed some issues with multiple active buffers
2009-08-27, by immler
clarified structure of TheoryView
2009-08-27, by immler
improved repainting
2009-08-27, by immler
tuned whitespace
2009-08-27, by immler
catching NPE on val
2009-08-27, by immler
Command and Command_State handle results from prover as Accumulator
2009-08-27, by immler
trait Accumulator;
2009-08-27, by immler
Command notifies changes
2009-08-27, by immler
change_receiver and output_info are used before regular initialisation
2009-08-27, by immler
TheoryView starts Prover
2009-08-27, by immler
output_info specific to prover
2009-08-27, by immler
proper activation with multiple buffers
2009-08-27, by immler
state_update global in Plugin
2009-08-27, by immler
unused
2009-08-27, by immler
fixed special case;
2009-08-27, by immler
added shortcut
2009-08-27, by immler
generalized settings;
2009-08-22, by wenzelm
Isabelle component;
2009-08-22, by wenzelm
less ambitious array operations -- for improved compatibility with older versions of bash;
2009-08-22, by wenzelm
Text is not present any more
2009-08-13, by immler
typo
2009-08-13, by immler
Change consisting of a list of Edits
2009-08-07, by immler
add is a private function
2009-08-03, by immler
avoid internal "add" method;
2009-07-27, by wenzelm
removed unused imports;
2009-07-27, by wenzelm
decode offsets with respect to symbols
2009-07-15, by immler
equal should be included
2009-07-15, by immler
arbitrary history
2009-07-13, by immler
commands carrying state-information
2009-07-08, by immler
gui element to set current document version
2009-07-08, by immler
set current document version; forget "future" versions in list
2009-07-08, by immler
current version in theoryview/buffer
2009-07-08, by immler
activation
2009-07-08, by immler
remember removed text
2009-07-08, by immler
insert mode isabelle into catalog
2009-07-08, by immler
updated to jedit 4.3pre17 -- no longer provide separate ml.xml;
2009-07-05, by wenzelm
updated to jEdit 4.3pre17;
2009-07-05, by wenzelm
removed obsolete isabelle.utils.Delay;
2009-07-05, by wenzelm
renamed Delay to clarified version Swing_Thread.delay;
2009-07-04, by wenzelm
change_receiver: removed redundant Swing_Thread wrapper -- the Delay timer action is already in Swing;
2009-07-04, by wenzelm
replaced utils.Delay by tune version isabelle.Delay (Pure.jar);
2009-07-04, by wenzelm
use symbolic NULL;
2009-07-04, by wenzelm
tuned token styles, according to some earlier Isabelle/jEdit experiments;
2009-07-04, by wenzelm
use static Map/Set for token categorization;
2009-07-04, by wenzelm
added symbol_index (presently unused);
2009-07-04, by wenzelm
misc tuning;
2009-07-04, by wenzelm
updated to Netbeans 6.7;
2009-07-03, by wenzelm
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
2009-06-30, by wenzelm
preload CSS resources;
2009-06-27, by wenzelm
more robust handling of Isabelle CSS files;
2009-06-26, by wenzelm
default file is plain Scratch.thy (as in Proof General);
2009-06-26, by wenzelm
removed obsolete VFS -- superceded by IsabelleEncoding;
2009-06-26, by wenzelm
prover.set_document: plain name, no path for now;
2009-06-26, by wenzelm
removes VFS service -- superceded by UTF-8-Isabelle encoding;
2009-06-26, by wenzelm
recovered Isabelle font -- deriveFont(Int) refers to style, not size!
2009-06-26, by wenzelm
opt-out obscure encodings;
2009-06-26, by wenzelm
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
2009-06-26, by wenzelm
decentralized Isabelle component names;
2009-06-26, by wenzelm
renamed UTF-8-isabelle to UTF-8-Isabelle;
2009-06-26, by wenzelm
pass JVM platform files, without going through the "isabelle:" VFS;
2009-06-26, by wenzelm
more precise wrapping of I/O streams;
2009-06-26, by wenzelm
some support for actual symbol recoding;
2009-06-25, by wenzelm
added IsabelleEncoding -- a clone of utf-8 for now;
2009-06-25, by wenzelm
added Boolean_Property, Int_Property;
2009-06-25, by wenzelm
simplified option pane: proper logic title, hardwired font path;
2009-06-25, by wenzelm
_canonPath: expand_path;
2009-06-25, by wenzelm
renamed IsabelleProcess to Isabelle_Process;
2009-06-25, by wenzelm
misc tuning and reorganization;
2009-06-25, by wenzelm
default sidekick.complete-delay;
2009-06-23, by wenzelm
fall back on Isabelle system completion (symbols only);
2009-06-23, by wenzelm
use isabelle.Completion;
2009-06-23, by wenzelm
acces position properties via Isabelle library;
2009-06-18, by wenzelm
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
2009-06-17, by wenzelm
basic keyword completions via isabelle.Scan.Lexicon;
2009-06-17, by wenzelm
minor tuning;
2009-06-16, by wenzelm
updated notes about Isabelle environment, no longer need to use "isabelle env netbeans";
2009-06-07, by wenzelm
static IsabelleSystem.charset (cf. http://isabelle.in.tum.de/repos/isabelle/rev/be0f7f4f9e12);
2009-06-07, by wenzelm
automated update by Scala plugin 6.7v1;
2009-06-04, by wenzelm
produce ids via Isabelle.system (http://isabelle.in.tum.de/repos/isabelle/rev/c23663825e23);
2009-06-04, by wenzelm
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
2009-06-04, by wenzelm
more robust get_offsets;
2009-06-04, by wenzelm
updates for Netbeans 6.7;
2009-06-03, by wenzelm
merged
2009-06-02, by wenzelm
merged
2009-06-02, by immler
merged; resolved superficial conflicts
2009-06-02, by immler
linearset works faster here
2009-06-02, by immler
lists work faster here
2009-06-02, by immler
fixed duplicate document-id
2009-06-02, by immler
ignore unchanged commands
2009-06-02, by immler
ignore unchanged tokens
2009-06-02, by immler
split change on activate
2009-06-02, by immler
return unchanged node on errors
2009-06-02, by immler
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
2009-06-02, by wenzelm
superficial tuning;
2009-06-02, by wenzelm
updated versions;
2009-06-02, by wenzelm
type_at: no quotes;
2009-06-02, by wenzelm
tuned;
2009-06-02, by wenzelm
use RichString.* to produce blanks;
2009-06-02, by wenzelm
change_receiver: start only once (already done in actor function);
2009-06-02, by wenzelm
superficial tuning;
2009-06-02, by wenzelm
slightly more robust treatment of options via arrays;
2009-05-30, by wenzelm
merged
2009-05-30, by wenzelm
outer syntax could clash with status on removed commands
2009-05-27, by immler
no null change
2009-05-27, by immler
fixed delete markup
2009-05-27, by immler
check presence of begin, end in attributes
2009-05-27, by immler
treat comments like seperate commands,
2009-05-27, by immler
split large changes for faster responses of prover
2009-05-27, by immler
changed handling of subdirectories
2009-05-25, by immler
more accurate setup for "jEdit" project;
2009-05-30, by wenzelm
recovered iso-latin-1 text;
2009-05-23, by wenzelm
improved handling of markup-information with command=null
2009-05-22, by immler
implemented links to other files
2009-05-22, by immler
implemented IsabelleHyperlinkSource (only links inside the current buffer)
2009-05-22, by immler
corrected offset
2009-05-22, by immler
fixed duplicate activation
2009-05-22, by immler
removed debug-painting
2009-05-22, by immler
let MarkupNode carry arbitrary information
2009-05-22, by immler
added hyperlink plugin
2009-05-22, by immler
ML types in tooltip
2009-05-22, by immler
chaned '+'
2009-05-22, by immler
reduced to one markup-tree
2009-05-22, by immler
implemented filter on markup-tree
2009-05-22, by immler
fixed flatten
2009-05-22, by immler
immutable markup-nodes;
2009-04-29, by immler
seperate node for syntax-highlighting
2009-04-27, by immler
included information on ML status messages in Sidekick's status-window
2009-04-27, by immler
abs. stops, markup nodes depend on doc-version;
2009-04-22, by immler
merged
2009-04-20, by immler
Anti-aliasing is now controlled via the smoothing threshhold
2009-04-20, by immler
incomplete changes of immutable tokens and commands
2009-04-20, by immler
prepared proofdocument for only needed changes
2009-04-16, by immler
use jEdits styles
2009-04-15, by immler
corrected displaying of phases in buffer with few lines;
2009-04-15, by immler
fixed shifting;
2009-04-14, by immler
correct order, added curreeeent change
2009-04-07, by immler
implemented to_current and from_current in dependancy of document-versions
2009-04-06, by immler
proofdocument-versions get id from changes
2009-04-06, by immler
when jEdit is run from Netbeans, activate=defer does not work (why?)
2009-03-28, by immler
merged: resolved conflicts with Markups: ML-syntax styles in styles.props
2009-03-23, by immler
changes of text with unique id
2009-03-20, by immler
fixes
2009-03-20, by immler
merged; resolved conflicts (kept own versions)
2009-03-19, by immler
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
2009-03-19, by immler
build jar before running/debugging
2009-03-19, by immler
probably setup from new Scala Plugin 0.15.1 for NetBeans
2009-03-19, by immler
LinearSet.prev
2009-03-19, by immler
merged, resolving minor conflicts;
2009-03-02, by wenzelm
preliminary/failed attempt to use the new IsarDocument access model to the prover;
2009-03-02, by wenzelm
ProofDocument without state
2009-03-08, by immler
*very* superficial usage of LinearSet
2009-03-05, by immler
implemented delete_after
2009-03-05, by immler
implemented insert_after
2009-03-05, by immler
changed title
2009-03-04, by immler
added Makarius' LinearSet
2009-03-04, by immler
tokens and commands as lists
2009-02-19, by immler
styles properties
2009-02-05, by immler
syntax styles in properties
2009-02-04, by immler
all token kinds have to be non-null
2009-02-04, by immler
removed redundant code
2009-02-04, by immler
added ML syntax markup;
2009-03-20, by wenzelm
less
more
|
(0)
-30000
-10000
-1920
+1920
+10000
+30000
tip