Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+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
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip