isabelle: Graph

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
2012-05-08, by bulwahn
prevent spurious timeouts
2012-05-07, by blanchet
added "try0" tool to Mirabelle
2012-05-07, by blanchet
use latest E (1.5)
2012-05-07, by blanchet
lifting package produces abs_eq_iff rules for total quotients
2012-05-04, by huffman
using the new transfer method to obtain abstract properties of RBT trees
2012-05-04, by bulwahn
back to post-release mode -- after fork point;
2012-05-02, by wenzelm
removed obsolete RC tags;
2012-05-23, by wenzelm
Added tag Isabelle2012 for changeset 21c42b095c84
2012-05-22, by wenzelm
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09); Isabelle2012
2012-05-20, by wenzelm
Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a
2012-05-17, by wenzelm
some message;
2012-05-17, by wenzelm
tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
2012-05-17, by wenzelm
Fixed disambiguation of names (cf. 5759ecd5c905)
2012-05-11, by berghofe
merged
2012-05-10, by wenzelm
file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;
2012-05-10, by wenzelm
prefer absolute paths, to allow launching from a different context (e.g. via file associations);
2012-05-10, by wenzelm
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
2012-05-10, by wenzelm
allow spaces in target directory;
2012-05-09, by wenzelm
Added tag Isabelle2012-RC2 for changeset 1636ff4c6243
2012-05-07, by wenzelm
init Cygwin after unpacking;
2012-05-07, by wenzelm
tuned proofs;
2012-05-06, by wenzelm
more accurate ROOT.ML;
2012-05-06, by wenzelm
prefer http://isabelle.in.tum.de/library alias, which is available at TUM only;
2012-05-06, by wenzelm
some highlights of Isabelle2012;
2012-05-05, by wenzelm
refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);
2012-05-04, by wenzelm
some attempts to make critical errors fit on screen;
2012-05-04, by wenzelm
more NEWS;
2012-05-03, by wenzelm
backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);
2012-05-03, by wenzelm
Added tag Isabelle2012-RC1 for changeset ec5d54029664
2012-05-02, by wenzelm
clarified;
2012-05-02, by wenzelm
makedist for release;
2012-05-02, by wenzelm
merged
2012-05-02, by wenzelm
more contributors;
2012-05-02, by wenzelm
tuned latex sources;
2012-05-02, by wenzelm
more CHECKLIST;
2012-05-02, by wenzelm
save 90MB by removing foreign binaries -- multi-platform installations are unlikely on Windows;
2012-05-02, by wenzelm
some re-ordering;
2012-05-02, by wenzelm
some re-ordering;
2012-05-02, by wenzelm
tuned spelling;
2012-05-02, by wenzelm
resolved maxidx bug
2012-05-02, by kuncar
documentation of the Lifting package on the ML level & tuned
2012-05-02, by kuncar
edit NEWS items for transfer/lifting
2012-05-02, by huffman
avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);
2012-05-02, by wenzelm
accomodate scala-2.10.0-M3 with its extra jar;
2012-05-02, by wenzelm
more robust wrt. spaces in directory names;
2012-05-02, by wenzelm
updated headers;
2012-05-02, by wenzelm
back to "Tools" in conformance with toplevel Isabelle layout (cf. 3fabf352243e, 15f4309bb9eb);
2012-05-02, by wenzelm
export more symbols
2012-04-30, by blanchet
merged
2012-04-30, by bulwahn
adding configuration to pass options to the ghc call in quickcheck[narrowing]
2012-04-30, by bulwahn
provide [[record_codegen]] option for skipping codegen setup for records
2012-04-30, by Gerwin Klein
making sorted_list_of_set executable
2012-04-30, by bulwahn
removing obsolete setup for sets now that sets are executable
2012-04-30, by bulwahn
update references in HOLCF README
2012-04-30, by huffman
basic setup for self-extracting 7zip installer;
2012-04-29, by wenzelm
merged
2012-04-29, by krauss
added test case for dependency graph (cf. 2d48bf79b725)
2012-04-29, by krauss
dependency graphs: fixed direction of edges
2012-04-29, by krauss
more CHECKLIST;
2012-04-29, by wenzelm
more windows-friendly presentation of main text files;
2012-04-29, by wenzelm
split into demo and competitive version
2012-04-29, by blanchet
Sledgehammer can do it
2012-04-29, by blanchet
compact nat literals
2012-04-29, by haftmann
some re-ordering;
2012-04-28, by wenzelm
some coverage of isabelle env;
2012-04-28, by wenzelm
updated system manual for release;
2012-04-28, by wenzelm
tuned;
2012-04-28, by wenzelm
some coverage of Isabelle/Scala tools;
2012-04-28, by wenzelm
some coverage of Isabelle/jEdit;
2012-04-28, by wenzelm
some manual updates;
2012-04-28, by wenzelm
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
2012-04-28, by wenzelm
add isar-ref documentation for transfer package
2012-04-28, by huffman
less confusion in NEWS
2012-04-28, by haftmann
rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly
2012-04-28, by haftmann
renamed Semi to Seq
2012-04-28, by nipkow
merged
2012-04-27, by wenzelm
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
2012-04-27, by wenzelm
clarified signature;
2012-04-27, by wenzelm
avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
2012-04-27, by wenzelm
made Context_Position independent from Config;
2012-04-27, by wenzelm
use Nitpick as an oracle for finite problems
2012-04-27, by blanchet
add extensionality to first-order provers
2012-04-27, by blanchet
avoid duplicate helpers
2012-04-27, by blanchet
mention tools and packages earlier;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
tuned;
2012-04-27, by wenzelm
merged
2012-04-27, by wenzelm
allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
2012-04-27, by huffman
documentation for the Lifting package in Isar-ref
2012-04-27, by kuncar
added darwin targets;
2012-04-27, by wenzelm
chmod -x;
2012-04-27, by wenzelm
multi-platform build script and component settings;
2012-04-27, by wenzelm
print errors on stderr;
2012-04-27, by wenzelm
general exec_process -- nothing specific to Cygwin;
2012-04-27, by wenzelm
more direct exec with synchronous exit code;
2012-04-27, by wenzelm
some updates on classic README, reduce the impression that there is much to install manually;
2012-04-27, by wenzelm
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
2012-04-27, by blanchet
move LEO-II closer to the top, for testing
2012-04-27, by blanchet
get rid of old CASC setup and move the arithmetic part to a new theory
2012-04-27, by blanchet
smaller batches, to play safe
2012-04-27, by blanchet
move file to where it belongs
2012-04-27, by blanchet
implement transfer tactic with more scalable forward proof methods
2012-04-27, by huffman
tuning
2012-04-27, by blanchet
tweak LEO-II setup
2012-04-27, by blanchet
eta-expand unapplied equalities in THF rather than using a proxy
2012-04-27, by blanchet
more tweaking of TPTP/CASC setup
2012-04-27, by blanchet
added a basic sanity check for quot_map
2012-04-26, by kuncar
tuned comment;
2012-04-26, by wenzelm
fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function
2012-04-26, by blanchet
merged
2012-04-26, by wenzelm
add code equation for real_of_float
2012-04-26, by hoelzl
tuned; don't generate abs code if quotient_type is used
2012-04-26, by kuncar
support Quotient map theorems with invariant parameters
2012-04-26, by kuncar
use a quot_map theorem attribute instead of the complicated map attribute
2012-04-26, by kuncar
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
2012-04-26, by blanchet
put Satallax first, at least for now (useful for experiments)
2012-04-26, by blanchet
tuning
2012-04-26, by blanchet
tuning
2012-04-26, by blanchet
tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
2012-04-26, by blanchet
tuning; no need for relevance filter
2012-04-26, by blanchet
tuning
2012-04-25, by blanchet
don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..."
2012-04-25, by blanchet
don't use the native choice operator if the type encoding isn't higher-order
2012-04-25, by blanchet
tuning
2012-04-25, by blanchet
more work on TPTP Isabelle and Sledgehammer tactics
2012-04-25, by blanchet
more work on CASC setup
2012-04-25, by blanchet
more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
2012-04-25, by wenzelm
mingw is windows (still inactive);
2012-04-25, by wenzelm
add Caratheodories theorem for semi-rings of sets
2012-04-25, by hoelzl
moved lemmas to appropriate places
2012-04-25, by hoelzl
register polyml executables so that Cygwin rebaseall will see them;
2012-04-25, by wenzelm
merged
2012-04-25, by wenzelm
smarter PDF_VIEWER defaults, based on hints by Lars Noschinski;
2012-04-25, by wenzelm
equate positive Lebesgue integral and MV-Analysis' Gauge integral
2012-04-25, by hoelzl
correct lemma name
2012-04-25, by hoelzl
tweak TPTP Nitpick's output
2012-04-25, by blanchet
remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1)
2012-04-25, by blanchet
improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things
2012-04-25, by blanchet
output SZS status as early as possible
2012-04-25, by blanchet
sorted lemma list in NEWS
2012-04-25, by hoelzl
merged
2012-04-25, by wenzelm
reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
2012-04-25, by wenzelm
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
2012-04-25, by wenzelm
updated README;
2012-04-25, by wenzelm
include generated application wrapper;
2012-04-25, by wenzelm
back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-25, by wenzelm
ISABELLE_JDK_HOME is already provided by isatest shell environment;
2012-04-25, by wenzelm
added splash screen, to reduce confusion when waiting for main application to start up;
2012-04-25, by wenzelm
move polyml within Cygwin /usr/local to simplify its rebasing;
2012-04-25, by wenzelm
improved spelling;
2012-04-25, by wenzelm
added "no_atp"s for extremely prolific, useless facts for ATPs
2012-04-25, by blanchet
tuned;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
made "split_last" more robust in the face of obscure low-level errors
2012-04-24, by blanchet
removed confusing error
2012-04-24, by blanchet
some friendly message;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by sultana
merged
2012-04-24, by sultana
reversed Tools to Actions Mirabelle renaming;
2012-04-24, by sultana
tuned;
2012-04-24, by sultana
reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
prefer evince over old xpdf -- NB: x86-cygwin bundles its own application;
2012-04-24, by wenzelm
cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
2012-04-24, by wenzelm
chmod -x;
2012-04-24, by wenzelm
augment Isabelle home directory more systematically;
2012-04-24, by wenzelm
Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version;
2012-04-24, by wenzelm
prevent change of directory, by pretending we are the "Command Here" utility;
2012-04-24, by wenzelm
typo
2012-04-24, by nipkow
the perennial doc problem of how to define lists a second time
2012-04-24, by nipkow
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
2012-04-24, by blanchet
updated doc
2012-04-24, by blanchet
add a timeout on the monotonicity check
2012-04-24, by blanchet
handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-24, by blanchet
get rid of old parser, hopefully for good
2012-04-24, by blanchet
fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")
2012-04-24, by blanchet
run Mirabelle in quick and dirty mode
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
scrollable text;
2012-04-23, by wenzelm
bundle Cygwin-Terminal.bat;
2012-04-23, by wenzelm
basic Cygwin-Terminal for main Isabelle directory;
2012-04-23, by wenzelm
moved to ~isatest/.bashrc to accomodate AFP;
2012-04-23, by wenzelm
merged
2012-04-23, by wenzelm
merged
2012-04-23, by nipkow
doc update
2012-04-23, by nipkow
NEWS
2012-04-23, by krauss
typedef with implicit set definition is considered legacy;
2012-04-23, by wenzelm
more standard method setup;
2012-04-23, by wenzelm
CONTRIBUTORS
2012-04-23, by kuncar
added useful Trueprop_conv
2012-04-23, by kuncar
move MRSL to a separate file
2012-04-23, by kuncar
avoid conflict of Isabelle vs. Isabelle.exe on Cygwin;
2012-04-23, by wenzelm
more notes on Cygwin, notably for downgrading to 1.7.9 to avoid multi-threading instabilities starting with 1.7.10 early 2012;
2012-04-23, by wenzelm
CONTRIBUTORS
2012-04-23, by hoelzl
reworked Probability theory
2012-04-23, by hoelzl
updated test;
2012-04-23, by sultana
improved non-interpretation of constants and numbers;
2012-04-23, by sultana
improved interpreting conditionals;
2012-04-23, by sultana
disabled interpreting arithmetic;
2012-04-23, by sultana
improved handling of single-quoted names;
2012-04-23, by sultana
disabled exception packaging in tptp;
2012-04-23, by sultana
moved function for testing problem-name parsing;
2012-04-23, by sultana
removed redundant function;
2012-04-23, by sultana
bundle Isabelle.exe;
2012-04-22, by wenzelm
tuned precedence order of transfer rules
2012-04-22, by huffman
updated generated files;
2012-04-22, by wenzelm
updated const "relcomp";
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
add transfer rule for set difference
2012-04-22, by huffman
support Cygwin cold-start via Isabelle.exe, assuming layout of bundle;
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
merged
2012-04-22, by huffman
adapt to changes in generated transfer rules (cf. 4483c004499a)
2012-04-22, by huffman
fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
2012-04-22, by huffman
more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
fixed typos
2012-04-22, by blanchet
tried harder to make SML/NJ happy
2012-04-22, by blanchet
added timeout argument to TPTP tools
2012-04-22, by blanchet
fix bug where "==" was used instead of "HOL.eq"
2012-04-22, by blanchet
more meaningful default value
2012-04-22, by blanchet
handle exception (needed to solve TPTP problem SEU880^5)
2012-04-22, by blanchet
pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;
2012-04-22, by wenzelm
refer to isabelle.Main application wrapper;
2012-04-22, by wenzelm
display return code like Isabelle.app on Mac OS;
2012-04-22, by wenzelm
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
2012-04-22, by wenzelm
updated Isabelle.exe specification, assuming layout of bundle;
2012-04-22, by wenzelm
USER_HOME settings variable points to cross-platform user home directory;
2012-04-22, by wenzelm
new example theory for quotient/transfer
2012-04-22, by huffman
update NEWS for transfer/quotient
2012-04-21, by huffman
enable variant of transfer method that proves an implication instead of an equivalence
2012-04-21, by huffman
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
2012-04-19, by haftmann
merged
2012-04-21, by wenzelm
NEWS for transfer, lifting, and quotient
2012-04-21, by huffman
new example theory for transfer package
2012-04-21, by huffman
some builtin session timing;
2012-04-21, by wenzelm
move alternative definition lemmas into Lifting.thy;
2012-04-21, by huffman
tuned proofs
2012-04-21, by huffman
add transfer rule for List.set
2012-04-21, by huffman
remove duplicate of lemma id_transfer
2012-04-21, by huffman
added covariant relator set_rel, with transfer rules for set operations
2012-04-21, by huffman
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
2012-04-21, by huffman
tried to make SML/NJ happy
2012-04-21, by blanchet
tuned "max_relevant" defaults for SMT solvers based on Judgment Day
2012-04-21, by blanchet
prepend PWD to relative paths
2012-04-21, by blanchet
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
2012-04-21, by blanchet
swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
2012-04-21, by blanchet
new transfer package rules and lifting setup for lists
2012-04-21, by huffman
strengthen rule list_all2_induct
2012-04-21, by huffman
more standard Theory_Data setup;
2012-04-20, by wenzelm
merged
2012-04-20, by wenzelm
add transfer rule for nat_case
2012-04-20, by huffman
uniform naming scheme for transfer rules
2012-04-20, by huffman
rename 'correspondence' method to 'transfer_prover'
2012-04-20, by huffman
hide the invariant constant for relators: invariant_commute infrastracture
2012-04-20, by kuncar
improved interleaving of start_execution vs. cancel_execution of the next update;
2012-04-20, by wenzelm
tuned proofs;
2012-04-20, by wenzelm
always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
2012-04-20, by wenzelm
tuned;
2012-04-20, by wenzelm
simplified internal actor protocol;
2012-04-20, by wenzelm
builtin timing for main operations;
2012-04-20, by wenzelm
add secondary transfer rule for universal quantifiers on non-bi-total relations
2012-04-20, by huffman
move definition of set_rel into Library/Quotient_Set.thy
2012-04-20, by huffman
add transfer rule for 'id'
2012-04-20, by huffman
add new transfer rules and setup for lifting package
2012-04-20, by huffman
setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
2012-04-20, by huffman
NEWS
2012-04-20, by hoelzl
hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-20, by hoelzl
merged
2012-04-20, by nipkow
forgot to add file
2012-04-20, by nipkow
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
2012-04-20, by huffman
merged
2012-04-19, by wenzelm
NEWS
2012-04-19, by hoelzl
transfer now handles Let
2012-04-19, by hoelzl
merged
2012-04-19, by nipkow
added revised version of Abs_Int
2012-04-19, by nipkow
add transfer rule for Let
2012-04-19, by huffman
add code lemmas for word operations
2012-04-19, by huffman
tuned whitespace
2012-04-19, by haftmann
dropped dead code
2012-04-19, by haftmann
rename no_code to no_abs_code - more appropriate name
2012-04-19, by kuncar
use tnames for bound variables in rsp thms
2012-04-19, by kuncar
true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-19, by blanchet
merged
2012-04-19, by blanchet
use latest Z3
2012-04-19, by blanchet
merged
2012-04-19, by nipkow
reorganised IMP
2012-04-19, by nipkow
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
2012-04-19, by hoelzl
use lifting to introduce floating point numbers
2012-04-18, by hoelzl
replace the float datatype by a type with unique representation
2012-04-18, by hoelzl
add lemmas to remove real conversions when compared to power of numerals
2012-04-18, by hoelzl
add simp rules to rewrite comparisons of 1 and real
2012-04-18, by hoelzl
add lemma to equate floor and div
2012-04-18, by hoelzl
add powr_inj
2012-04-18, by hoelzl
add lemmas to rewrite powr to power
2012-04-18, by hoelzl
add lemmas to compare log with 0 and 1
2012-04-18, by hoelzl
add ceiling_diff_floor_le_1
2012-04-18, by hoelzl
display Java 7 only code for now (cf. b9e2ed4b1579);
2012-04-19, by wenzelm
some sidekick options for more advanced completion;
2012-04-19, by wenzelm
custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
2012-04-19, by wenzelm
tuned imports;
2012-04-19, by wenzelm
more robust wrt. exceptions;
2012-04-19, by wenzelm
accomodate digits within Isar command names, notably 'try0';
2012-04-19, by wenzelm
more robust Sledgehammer in Prover IDE;
2012-04-19, by wenzelm
test with jdk-7u3 that is also bundled;
2012-04-19, by wenzelm
create thm names correctly
2012-04-19, by kuncar
updated components according to tentative bundle;
2012-04-19, by wenzelm
back to isatest with official polyml-5.4.1 (cf. ffa6e10df091);
2012-04-19, by wenzelm
use simpler method for preserving bound variable names in transfer tactic
2012-04-19, by huffman
tuned lemmas (v)image_id;
2012-04-19, by huffman
use latest SPASS
2012-04-19, by blanchet
doc update
2012-04-19, by blanchet
dropped dead code;
2012-04-19, by haftmann
generate abs_induct rules for quotient types
2012-04-19, by huffman
tuned
2012-04-19, by haftmann
corrected Nbe.static_value: ignore cached compilations;
2012-04-19, by haftmann
tuned heading
2012-04-19, by haftmann
tuned name
2012-04-18, by haftmann
improved threading of thy-values through interpret functions;
2012-04-19, by sultana
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
2012-04-19, by sultana
add option to transfer method for specifying variables not to generalize over
2012-04-18, by huffman
New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-17, by Thomas Sewell
setup_lifting: no_code switch and supoport for quotient theorems
2012-04-18, by kuncar
remove old TPTP CNF/FOF parser; always use Nik's new parser
2012-04-18, by blanchet
more standard SZS output
2012-04-18, by blanchet
Sledgehammer NEWS and CONTRIBUTORS
2012-04-18, by blanchet
tuned SZS status output
2012-04-18, by blanchet
update documentation (mostly based on feedback by Makarius)
2012-04-18, by blanchet
added SZS status wrappers in TPTP mode
2012-04-18, by blanchet
fixed Auto Nitpick's output
2012-04-18, by blanchet
phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup
2012-04-18, by blanchet
started integrating Nik's parser into TPTP command-line tools
2012-04-18, by blanchet
merged
2012-04-18, by wenzelm
tuned
2012-04-18, by haftmann
dropped errorneous NEWS entry
2012-04-18, by haftmann
merged
2012-04-18, by wenzelm
consolidated NEWS entries on fold
2012-04-18, by haftmann
grouped fold-related NEWS entries together
2012-04-18, by haftmann
grouped NEWS concerning relations together
2012-04-18, by haftmann
merged rename traces
2012-04-18, by haftmann
fixed type interpretation;
2012-04-18, by sultana
more tptp testing support functions;
2012-04-18, by sultana
tuned text, improved dependencies
2012-04-18, by nipkow
Lifting: generate more thms & note them & tuned
2012-04-18, by kuncar
move constant 'Respects' into Lifting.thy;
2012-04-18, by huffman
more friendly sendback rendering, using green and "frisches Steingrau";
2012-04-18, by wenzelm
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
2012-04-18, by wenzelm
approximative file position for Pure entities;
2012-04-18, by wenzelm
render last ML_TYPING only -- relevant for inline antiquotations like @{term};
2012-04-18, by wenzelm
flat presentation of collective markup;
2012-04-18, by wenzelm
add lemma Quotient_abs_induct
2012-04-18, by huffman
more usage of context blocks
2012-04-18, by huffman
use context block
2012-04-18, by huffman
lifting_setup generates transfer rule for rep of typedefs
2012-04-18, by huffman
use context block to organize typedef lifting theorems
2012-04-18, by huffman
avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
2012-04-18, by blanchet
compile
2012-04-18, by blanchet
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
2012-04-18, by blanchet
doc update
2012-04-18, by blanchet
display more messages, now that more provers are run by default
2012-04-18, by blanchet
added testing of tptp problem names;
2012-04-17, by sultana
tidied exception-handling relating to tptp problem names;
2012-04-17, by sultana
updated TPTP's ROOT.ML to include TPTP_Interpret;
2012-04-17, by sultana
retain ISABELLE_HOME_WINDOWS which is useful for jEdit to fold file names symbolically, but without DOS expansion that causes problems with Cygwin/Posix roundtrip (cf. 5a7903ba2dac);
2012-04-17, by wenzelm
updated to scala-2.9.2;
2012-04-17, by wenzelm
make transfer method more deterministic by using SOLVED' on some subgoals
2012-04-17, by huffman
accomodate ProofGeneral as Isabelle component, with adhoc version switch for Cygwin as before;
2012-04-17, by wenzelm
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
2012-04-17, by kuncar
improved exception-handling in tptp;
2012-04-17, by sultana
simplified interpretation of '$i';
2012-04-17, by sultana
more cleaning of tptp tests;
2012-04-17, by sultana
improved tptp_graph robustness by relying on thy;
2012-04-17, by sultana
improved tptp interpretation test thy
2012-04-17, by sultana
tuned comments
2012-04-17, by sultana
improved handling of quoted names in tptp import
2012-04-17, by sultana
improved naming of 'distinct objects' in tptp import
2012-04-17, by sultana
reorganised tptp testing thys
2012-04-17, by sultana
enforced 'include' restrictions
2012-04-17, by sultana
tuned
2012-04-17, by sultana
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
2012-04-17, by sultana
updated rel_comp ~> relcomp (cf. e1b761c216ac);
2012-04-17, by wenzelm
merged
2012-04-17, by blanchet
more helpful error message
2012-04-17, by blanchet
avoid option introduced in E 1.2 when invoking older versions of E
2012-04-17, by blanchet
go back to the explicit compisition of quotient theorems
2012-04-17, by kuncar
add theory data for relator identity rules;
2012-04-17, by huffman
note the Quotient theorem in quotient_type
2012-04-17, by kuncar
leave Lifting prefix
2012-04-16, by kuncar
more user aliases;
2012-04-16, by wenzelm
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
2012-04-16, by wenzelm
updated and clarified OF/MRS;
2012-04-16, by wenzelm
document attribute "abs_def";
2012-04-16, by wenzelm
repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);
2012-04-16, by wenzelm
merged
2012-04-16, by nipkow
refined new tutorial announcement
2012-04-04, by nipkow
merged
2012-04-16, by bulwahn
duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
2012-04-16, by Christian Sternagel
updated for release;
2012-04-16, by wenzelm
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
2012-04-16, by wenzelm
tuned some proofs;
2012-04-16, by huffman
centralized enriched_type declaration, thanks to in-situ available Isar commands
2012-04-15, by haftmann
tuned whitespace
2012-04-15, by haftmann
replace locale 'UFT' with new un-named context block feature;
2012-04-15, by huffman
more CONTRIBUTORS;
2012-04-15, by wenzelm
some coverage of bundled declarations;
2012-04-15, by wenzelm
more uniform outline;
2012-04-15, by wenzelm
some coverage of unnamed contexts, which can be nested within other targets;
2012-04-15, by wenzelm
gathered mirabelle_sledgehammer's hardcoded defaults
2012-04-14, by sultana
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
2012-04-14, by sultana
Mirabelle now gives usage info when no arguments given
2012-04-14, by sultana
switched from using sed to perl in mirabelle tool
2012-04-14, by sultana
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
2012-04-14, by sultana
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
2012-04-14, by wenzelm
merged;
2012-04-14, by wenzelm
removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
2012-04-14, by krauss
aligned tptp_graph dependencies to Isabelle conventions;
2012-04-14, by sultana
more ambitious isatest settings using polyml-svn (e.g. 1487);
2012-04-14, by wenzelm
use official TextArea.isCaretVisible and thus follow the "blink" flag;
2012-04-14, by wenzelm
display more memory;
2012-04-14, by wenzelm
keyword ";" is declared via prover (as "minor", not "diag");
2012-04-14, by wenzelm
outermost SELECT_GOAL potentially improves performance;
2012-04-14, by wenzelm
report ISABELLE_HOME_WINDOWS;
2012-04-14, by wenzelm
chmod +x;
2012-04-14, by wenzelm
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
2012-04-14, by wenzelm
misc tuning for release;
2012-04-14, by wenzelm
revert changes of already published NEWS;
2012-04-14, by wenzelm
some updates for release;
2012-04-14, by wenzelm
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
2012-04-14, by wenzelm
updated Scala/JVM versions;
2012-04-14, by wenzelm
include trailing comments in proper_command range;
2012-04-13, by wenzelm
minimal support for x86-mingw;
2012-04-13, by wenzelm
recognize MacOS on modern Java implementations, notably OpenJDK 1.7;
2012-04-13, by wenzelm
updated to Scala 2.9.2;
2012-04-13, by wenzelm
updated headers;
2012-04-13, by wenzelm
eliminated hard tabs;
2012-04-13, by wenzelm
Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2012-04-13, by Andreas Lochbihler
NEWS
2012-04-13, by Andreas Lochbihler
adapt to changes in RBT_Impl
2012-04-13, by Andreas Lochbihler
move RBT implementation into type class contexts
2012-04-13, by Andreas Lochbihler
misc tuning;
2012-04-13, by wenzelm
NEWS
2012-04-13, by bulwahn
merged
2012-04-12, by krauss
distributivity of * over Un and UNION
2012-04-12, by krauss
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
2012-04-12, by krauss
removed "setsum_set", now subsumed by generic setsum
2012-04-12, by krauss
backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)
2012-04-12, by krauss
tuned README;
2012-04-12, by wenzelm
direct scala toplevel tools to ISABELLE_JDK_HOME;
2012-04-12, by wenzelm
simplified component structure;
2012-04-12, by wenzelm
merged
2012-04-12, by wenzelm
merged
2012-04-12, by Andreas Lochbihler
generalise case certificates to allow ignored parameters
2012-04-12, by Andreas Lochbihler
merged
2012-04-12, by bulwahn
manual merge
2012-04-04, by griff
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-03, by griff
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-03, by griff
more standard method setup;
2012-04-12, by wenzelm
more precise declaration of goal_tfrees in forked proof state;
2012-04-12, by wenzelm
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
2012-04-12, by wenzelm
multiset operations are defined with lift_definitions;
2012-04-12, by bulwahn
remove outdated comment
2012-04-12, by huffman
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-04-11, by wenzelm
standardized ML aliases;
2012-04-11, by wenzelm
clarified proof_result: finish proof formally via head tr, not end_tr;
2012-04-11, by wenzelm
tuned;
2012-04-11, by wenzelm
more robust Future.fulfill wrt. duplicate assignment and interrupt;
2012-04-11, by wenzelm
tuned message;
2012-04-11, by wenzelm
always signal after cancel_group: passive tasks may have become active;
2012-04-11, by wenzelm
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
2012-04-11, by wenzelm
merged
2012-04-10, by wenzelm
moved lift_raw_const wrapper out of the Quotient-package into Nominal2
2012-04-10, by Christian Urban
misc tuning and simplification;
2012-04-10, by wenzelm
static relevance of proof via syntax keywords;
2012-04-10, by wenzelm
tuned future priorities: print 0, goal ~1, execute ~2;
2012-04-10, by wenzelm
updated for Poly/ML SVN 1476;
2012-04-10, by wenzelm
some coverage of HOL/TPTP;
2012-04-10, by wenzelm
added graph-conversion utility for TPTP files
2012-04-10, by sultana
moved non-interpret-specific code to different module
2012-04-10, by sultana
disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
2012-04-09, by wenzelm
tuned proofs;
2012-04-09, by wenzelm
slightly faster default compilation of Isabelle/Scala;
2012-04-09, by wenzelm
more explicit last exec result;
2012-04-09, by wenzelm
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
2012-04-09, by wenzelm
tuned;
2012-04-09, by wenzelm
simplified Future.cancel/cancel_group (again) -- running threads only;
2012-04-09, by wenzelm
added ML pretty-printing;
2012-04-09, by wenzelm
merged
2012-04-07, by wenzelm
merged
2012-04-07, by wenzelm
explicit constructor Nat leaves nat_of as conversion
2012-04-07, by haftmann
abandoned almost redundant *_foldr lemmas
2012-04-06, by haftmann
tuned
2012-04-06, by haftmann
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-04-06, by haftmann
enable parallel proofs (cf. e8552cba702d), only affects packages so far;
2012-04-07, by wenzelm
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07, by wenzelm
tuned proofs;
2012-04-07, by wenzelm
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
2012-04-07, by wenzelm
tuned imports;
2012-04-07, by wenzelm
updated header keywords;
2012-04-07, by wenzelm
init message not bad;
2012-04-07, by wenzelm
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
2012-04-07, by wenzelm
discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06, by wenzelm
remove now-unnecessary type annotations from lift_definition commands
2012-04-06, by huffman
more robust generation of quotient rules using tactics
2012-04-06, by huffman
merged
2012-04-06, by huffman
add function dest_Quotient
2012-04-06, by huffman
standardized alias;
2012-04-06, by wenzelm
fixed document;
2012-04-06, by wenzelm
merged
2012-04-06, by wenzelm
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
2012-04-06, by huffman
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
2012-04-05, by kuncar
make Quotient_Def.lift_raw_const working again
2012-04-05, by kuncar
use standard quotient lemmas to generate transfer rules
2012-04-05, by huffman
add transfer lemmas for quotients
2012-04-05, by huffman
define reflp directly, in the manner of symp and transp
2012-04-05, by huffman
set up and use lift_definition for word operations
2012-04-05, by huffman
lift_definition declares transfer_rule attribute
2012-04-05, by huffman
configure transfer method for 'a word -> int
2012-04-05, by huffman
added timestamps to logging of named thms
2012-04-05, by krauss
merged
2012-04-05, by huffman
merged
2012-04-04, by huffman
add lemmas for generating transfer rules for typedefs
2012-04-04, by huffman
tuned;
2012-04-05, by sultana
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
2012-04-04, by sultana
merge
2012-04-04, by Cezary Kaliszyk
HOL/Import more precise map types
2012-04-04, by Cezary Kaliszyk
HOL/Import typed matches against Isabelle typedef result
2012-04-04, by Cezary Kaliszyk
connect the Quotient package to the Lifting package
2012-04-04, by kuncar
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04, by kuncar
tuned;
2012-04-04, by sultana
added interpretation for formula conditional;
2012-04-04, by sultana
refactored tptp lex;
2012-04-04, by sultana
refactored tptp yacc to bring close to official spec;
2012-04-04, by sultana
transfer method generalizes over free variables in goal
2012-04-04, by huffman
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-04, by huffman
update keywords file
2012-04-04, by huffman
merged
2012-04-04, by huffman
fix typos
2012-04-04, by huffman
lift_definition command generates transfer rule
2012-04-04, by huffman
prove_quot_theorem fixes types
2012-04-04, by huffman
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
2012-04-04, by bulwahn
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
2012-04-04, by bulwahn
stop node execution at first unassigned exec;
2012-04-06, by wenzelm
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-06, by wenzelm
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
2012-04-05, by wenzelm
less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05, by wenzelm
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05, by wenzelm
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
2012-04-05, by wenzelm
Command.memo including physical interrupts (unlike Lazy.lazy);
2012-04-05, by wenzelm
tuned;
2012-04-05, by wenzelm
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04, by wenzelm
proper signature constraint;
2012-04-04, by wenzelm
tuned comments;
2012-04-04, by wenzelm
separate module for prover command execution;
2012-04-04, by wenzelm
tuned;
2012-04-04, by wenzelm
fix typo in ML structure name
2012-04-04, by huffman
removed obsolete isar-overview manual;
2012-04-04, by wenzelm
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
2012-04-04, by sultana
merged
2012-04-04, by bulwahn
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-04-04, by bulwahn
improved equality check for modes in predicate compiler
2012-04-04, by bulwahn
rename ML structure to avoid shadowing earlier name
2012-04-04, by huffman
add type annotations to make SML happy (cf. ec6187036495)
2012-04-04, by huffman
merged
2012-04-03, by huffman
new transfer proof method
2012-04-03, by huffman
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03, by huffman
prefer prog-prove, suppress isar-overview;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
formal integration of "prog-prove" manual;
2012-04-03, by wenzelm
prefer static dependencies;
2012-04-03, by wenzelm
merged
2012-04-03, by huffman
modernized obsolete old-style theory name with proper new-style underscore
2012-04-03, by huffman
removed use of CharVector in generated parser, to make SMLNJ happy
2012-04-03, by sultana
avoid duplicate PIDE markup;
2012-04-03, by wenzelm
less intrusive visibility;
2012-04-03, by wenzelm
more robust re-import wrt. non-HHF assumptions;
2012-04-03, by wenzelm
consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
2012-04-03, by wenzelm
close context elements via Expression.cert/read_declaration;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
added me to isatest email list
2012-04-03, by sultana
new package Lifting - initial commit
2012-04-03, by kuncar
add floor/ceiling lemmas suggested by René Thiemann
2012-04-03, by huffman
made sure that " is shown in tutorial text
2012-04-03, by nipkow
merged
2012-04-02, by Christian Urban
tuned proofs
2012-04-02, by Christian Urban
merged
2012-04-02, by nipkow
towards showing " in the tutorial
2012-04-02, by nipkow
tuned proof in order to avoid warning message
2012-04-02, by Christian Urban
remove unnecessary qualifiers on names
2012-04-02, by huffman
add lemma Suc_1
2012-04-02, by huffman
merged
2012-04-02, by berghofe
Require "For" keyword to be followed by at least one whitespace, to avoid that
2012-04-02, by berghofe
normalize defs (again, cf. 008b7858f3c0);
2012-04-03, by wenzelm
some context examples;
2012-04-03, by wenzelm
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
2012-04-03, by wenzelm
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
2012-04-03, by wenzelm
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
2012-04-03, by wenzelm
better drop background syntax if entity depends on parameters;
2012-04-03, by wenzelm
more uniform abbrev vs. define;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
clarified generic_const vs. close_schematic_term;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more uniform theory_abbrev with const_declaration;
2012-04-03, by wenzelm
avoid const_declaration in aux. context (cf. locale_foundation);
2012-04-03, by wenzelm
clarified background_foundation vs. theory_foundation (with const_declaration);
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more general standard_declaration;
2012-04-02, by wenzelm
better restore after close_target;
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
clarified standard_declaration vs. theory_declaration;
2012-04-02, by wenzelm
smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
tuned;
2012-04-02, by wenzelm
tuned signature;
2012-04-02, by wenzelm
misc tuning and simplification;
2012-04-02, by wenzelm
better restore to first target, not last target;
2012-04-02, by wenzelm
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
2012-04-02, by wenzelm
more general Local_Theory.restore, allow any nesting level;
2012-04-02, by wenzelm
new tutorial
2012-04-02, by nipkow
New manual Programming and Proving in Isabelle/HOL
2012-04-02, by nipkow
add simp rules for dvd on negative numerals
2012-04-02, by huffman
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
2012-04-01, by krauss
clarified terminology; added reference to bundle component
2012-04-01, by krauss
less modest NEWS; CONTRIBUTORS
2012-04-01, by krauss
renamed import session back to Import, conforming to directory name; NEWS
2012-04-01, by krauss
more precise IsaMakefile (eg. see HOL-Algebra);
2012-04-01, by wenzelm
more keywords;
2012-04-01, by wenzelm
merged
2012-04-01, by wenzelm
merged
2012-04-01, by krauss
removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare
2012-04-01, by krauss
Modernized HOL-Import for HOL Light
2012-04-01, by Cezary Kaliszyk
merged
2012-04-01, by wenzelm
adapted Mira configuration to dd04c8173bb2.
2012-04-01, by krauss
removed Nat_Numeral.thy, moving all theorems elsewhere
2012-04-01, by huffman
less brutal return from function, to allow caller to report error;
2012-04-01, by wenzelm
more general context command with auxiliary fixes/assumes etc.;
2012-04-01, by wenzelm
more precise type annotation (cf. 6523a21076a8);
2012-04-01, by wenzelm
nothing specific about named target;
2012-04-01, by wenzelm
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
2012-04-01, by wenzelm
added Attrib.global_notes/local_notes/generic_notes convenience;
2012-04-01, by wenzelm
simplified;
2012-04-01, by wenzelm
tuned signature;
2012-04-01, by wenzelm
clarified Named_Target.target_declaration: propagate through other levels as well;
2012-04-01, by wenzelm
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
2012-04-01, by wenzelm
tuned proofs
2012-04-01, by huffman
merged
2012-03-31, by huffman
tuned proof
2012-03-31, by huffman
add lemma power_le_one
2012-03-31, by huffman
tuned;
2012-03-31, by wenzelm
tuned signature;
2012-03-31, by wenzelm
more direct Local_Defs.contract;
2012-03-31, by wenzelm
more precise Local_Defs.expand wrt. *local* prems only;
2012-03-31, by wenzelm
tuned comment;
2012-03-31, by wenzelm
more robust Scala 2.9.x interpreter invocation -- avoid separate interpreter thread and thus deadlock of Swing_Thread.now;
2012-03-30, by wenzelm
tuned;
2012-03-30, by wenzelm
dropped empty files
2012-03-30, by haftmann
dropped now obsolete Cset theories
2012-03-30, by haftmann
merged
2012-03-30, by wenzelm
tuned proofs, less guesswork;
2012-03-30, by wenzelm
merged
2012-03-30, by huffman
load Tools/numeral.ML in Num.thy
2012-03-30, by huffman
tuned proof
2012-03-30, by huffman
set up numeral reorient simproc in Num.thy
2012-03-30, by huffman
remove redundant simp rule
2012-03-30, by huffman
add simp rules for eve/odd on numerals
2012-03-30, by huffman
remove content-free theory ex/Arithmetic_Series_Complex.thy
2012-03-30, by huffman
rephrase lemmas about arithmetic series using numeral '2'
2012-03-30, by huffman
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-03-30, by huffman
replace lemmas eval_nat_numeral with a simpler reformulation
2012-03-30, by huffman
restate various simp rules for word operations using pred_numeral
2012-03-30, by huffman
new lemmas for simplifying subtraction on nat numerals
2012-03-30, by huffman
removed redundant nat-specific copies of theorems
2012-03-30, by huffman
move more theorems from Nat_Numeral.thy to Num.thy
2012-03-30, by huffman
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
2012-03-30, by wenzelm
more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);
2012-03-30, by wenzelm
more explicit isatest environment settings (from private .bashrc);
2012-03-30, by wenzelm
merged
2012-03-30, by huffman
fix search-and-replace errors
2012-03-30, by huffman
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
2012-03-30, by huffman
add constant pred_numeral k = numeral k - (1::nat);
2012-03-30, by huffman
move lemmas from Nat_Numeral.thy to Nat.thy
2012-03-30, by huffman
move lemmas from Nat_Numeral to Int.thy and Num.thy
2012-03-30, by huffman
merged
2012-03-30, by bulwahn
adding theory to prove completeness of the exhaustive generators
2012-03-30, by bulwahn
refine bindings in quickcheck_common: do not conceal and do not declare as simps
2012-03-30, by bulwahn
hiding fact not so aggressively
2012-03-30, by bulwahn
power on predicate relations
2012-03-30, by haftmann
made Mirabelle-SH's 'trivial' check optional;
2012-03-30, by sultana
merged
2012-03-29, by wenzelm
more specific notion of partiality (cf. Scala version);
2012-03-29, by wenzelm
use qualified names for rsp and rep_eq theorems in quotient_def
2012-03-29, by kuncar
announcing NEWS (cf. 446cfc760ccf)
2012-03-29, by bulwahn
remove obsolete simp rule for powers
2012-03-29, by huffman
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
2012-03-29, by huffman
remove unneeded rewrite rules for powers of numerals
2012-03-29, by huffman
remove duplicate lemma Suc_numeral
2012-03-29, by huffman
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
2012-03-29, by huffman
bootstrap Num.thy before Power.thy;
2012-03-29, by huffman
educated guess to include jdk
2012-03-29, by haftmann
improved robustness with new antiquoation by Makarius
2012-03-28, by nipkow
merged
2012-03-28, by nipkow
updates
2012-03-28, by nipkow
updated documentation files (cf. c14fda8fee38)
2012-03-28, by bulwahn
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
2012-03-28, by wenzelm
merged
2012-03-28, by wenzelm
removed references to obsolete theorems
2012-03-28, by huffman
merged
2012-03-28, by bulwahn
some tuning while reviewing the current state of the quotient_def package
2012-03-28, by bulwahn
improving spelling
2012-03-28, by bulwahn
changing more definitions to quotient_definition
2012-03-28, by bulwahn
removing now redundant impl_of theorems in DAList
2012-03-28, by bulwahn
using abstract code equations for proofs of code equations in Multiset
2012-03-28, by bulwahn
simplified statements and proofs;
2012-03-28, by wenzelm
tuned whitespace;
2012-03-28, by wenzelm
updated Sign.add_type, Name_Space.declare;
2012-03-28, by wenzelm
updated comments;
2012-03-28, by wenzelm
merged
2012-03-28, by huffman
remove unnecessary rules from the simpset
2012-03-27, by huffman
remove unused premises
2012-03-27, by huffman
remove duplicate lemmas
2012-03-27, by huffman
mark some duplicate lemmas for deletion
2012-03-27, by huffman
remove more redundant lemmas
2012-03-27, by huffman
tuned proofs
2012-03-27, by huffman
remove redundant lemmas
2012-03-27, by huffman
generalized lemma zpower_zmod
2012-03-27, by huffman
remove redundant lemma
2012-03-27, by huffman
remove redundant lemma
2012-03-27, by huffman
remove duplicate [algebra] declarations
2012-03-27, by huffman
generalize more div/mod lemmas
2012-03-27, by huffman
generalize some theorems about div/mod
2012-03-27, by huffman
updated to jedit-4.5.1;
2012-03-28, by wenzelm
merged
2012-03-27, by kuncar
note a code eqn in quotient_def
2012-03-27, by kuncar
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-27, by boehmes
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
2012-03-27, by blanchet
fixed eta-extension of higher-order quantifiers in THF output
2012-03-27, by blanchet
renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-27, by blanchet
tuning
2012-03-27, by blanchet
tuning (in particular, Symtab instead of AList)
2012-03-27, by blanchet
tweak slices, based on eval by Daniel Wand
2012-03-27, by blanchet
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
2012-03-27, by blanchet
print a hint
2012-03-27, by blanchet
avoid DL
2012-03-27, by blanchet
TFF: declare free types as types
2012-03-27, by blanchet
merged
2012-03-27, by bulwahn
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
2012-03-27, by bulwahn
remove redundant lemmas
2012-03-27, by huffman
move int::ring_div instance upward, simplify several proofs
2012-03-27, by huffman
rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
2012-03-27, by huffman
extend definition of divmod_int_rel to handle denominator=0 case
2012-03-27, by huffman
tuned proofs
2012-03-27, by huffman
shorten a proof
2012-03-27, by huffman
simplify some proofs
2012-03-27, by huffman
rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
2012-03-27, by huffman
simplify some proofs
2012-03-27, by huffman
merged
2012-03-26, by wenzelm
merged
2012-03-26, by nipkow
reverted to canonical name
2012-03-26, by nipkow
merged
2012-03-26, by wenzelm
merged
2012-03-26, by huffman
revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
2012-03-26, by huffman
merged
2012-03-26, by huffman
fix incorrect code_modulename declarations
2012-03-26, by huffman
code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
2012-03-26, by huffman
remove old-style semicolon
2012-03-26, by huffman
merged
2012-03-26, by nipkow
Functions and lemmas by Christian Sternagel
2012-03-26, by nipkow
more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
2012-03-26, by wenzelm
disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
2012-03-26, by wenzelm
tuned comment
2012-03-26, by kuncar
merged
2012-03-26, by kuncar
merged
2012-03-26, by kuncar
tuned proof - no smt call
2012-03-26, by kuncar
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
2012-03-26, by wenzelm
updated theory header syntax and related details;
2012-03-26, by wenzelm
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
2012-03-24, by wenzelm
merged
2012-03-26, by wenzelm
reintroduced broken proofs and regenerated certificates
2012-03-26, by blanchet
merged, resolving trivial conflict;
2012-03-26, by wenzelm
fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-26, by blanchet
merged fork with new numeral representation (see NEWS)
2012-03-25, by huffman
merged
2012-03-24, by kuncar
use Thm.transfer for thms stored in generic context data storage
2012-03-23, by kuncar
hide invariant constant
2012-03-23, by kuncar
explicit SMTP server (appears to be required after recent change of system configuration);
2012-03-24, by wenzelm
more isatest subscribers;
2012-03-24, by wenzelm
merged
2012-03-23, by paulson
proof tidying
2012-03-23, by paulson
updated comment
2012-01-16, by kuncar
resolve invariant constant name clash
2012-03-23, by kuncar
update etc/isar-keywords.el
2012-03-23, by kuncar
fix example files
2012-03-23, by kuncar
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
2012-03-23, by kuncar
simplified code of generation of aggregate relations
2012-03-23, by kuncar
store the relational theorem for every relator
2012-03-23, by kuncar
store the quotient theorem for every quotient
2012-03-23, by kuncar
fix Quotient_Examples
2012-03-23, by kuncar
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
2012-03-23, by kuncar
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
2012-03-23, by bulwahn
tuned;
2012-03-23, by wenzelm
merged;
2012-03-22, by wenzelm
fixed typo
2012-03-22, by haftmann
more instructive NEWS
2012-03-22, by haftmann
more structured proofs
2012-03-22, by paulson
New Message
2012-03-22, by paulson
No longer treat "title" as FDL keyword
2012-03-22, by berghofe
tuned proofs;
2012-03-22, by wenzelm
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
synchronize syntax uniformly for target stack and aux. context;
2012-03-22, by wenzelm
tuned;
2012-03-22, by wenzelm
merged
2012-03-21, by wenzelm
removed Satallax option, now that this is the default
2012-03-21, by blanchet
doc update
2012-03-21, by blanchet
improve "remote_satallax" by exploiting unsat core
2012-03-21, by blanchet
generate weights and precedences for predicates as well
2012-03-21, by blanchet
refinements to constructibility
2012-03-21, by paulson
More structured proofs for infinite cardinalities
2012-03-21, by paulson
actually expose target context;
2012-03-21, by wenzelm
more explicit Toplevel.open_target/close_target;
2012-03-21, by wenzelm
tuned signature;
2012-03-21, by wenzelm
optional 'includes' element for long theorem statements;
2012-03-21, by wenzelm
basic support for nested contexts including bundles;
2012-03-21, by wenzelm
tuned messages;
2012-03-21, by wenzelm
basic support for nested local theory targets;
2012-03-21, by wenzelm
try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;
2012-03-21, by wenzelm
improved isatest arguments for macbroy2;
2012-03-21, by wenzelm
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
2012-03-21, by wenzelm
prefer explicitly qualified exception List.Empty;
2012-03-21, by wenzelm
merged
2012-03-20, by wenzelm
refined init_model: allow change of buffer name as caused by "Save as", for example;
2012-03-20, by wenzelm
basic support for bundled declarations;
2012-03-20, by wenzelm
doc update
2012-03-20, by blanchet
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
2012-03-20, by blanchet
removed obsolete temporary hack
2012-03-20, by blanchet
tweaks
2012-03-20, by blanchet
proof tidying
2012-03-20, by paulson
minimalistic support for remote URLs: no master dir here;
2012-03-20, by wenzelm
optimized "metis" call
2012-03-20, by blanchet
added term_order option to Mirabelle
2012-03-20, by blanchet
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
2012-03-20, by blanchet
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
2012-03-20, by blanchet
remove two options that were found to play hardly any role
2012-03-20, by blanchet
enable "metis_advisory_simp" by default
2012-03-20, by blanchet
more stats;
2012-03-20, by wenzelm
merged
2012-03-20, by paulson
more structured proofs
2012-03-20, by paulson
don't generate new SPASS constructs for old SPASS
2012-03-20, by blanchet
tune Metis example
2012-03-20, by blanchet
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-03-20, by blanchet
continued implementation of term ordering attributes
2012-03-20, by blanchet
added "dont_preplay" alias
2012-03-20, by blanchet
document "dont_preplay"
2012-03-20, by blanchet
tuning
2012-03-20, by blanchet
implement term order attribute (for experiments)
2012-03-20, by blanchet
tuning -- don't refer to old, internal version number (needlessly confusing now)
2012-03-20, by blanchet
more weight attribute tuning
2012-03-20, by blanchet
use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
2012-03-20, by blanchet
internal renamings
2012-03-20, by blanchet
renamed E weight attribute
2012-03-20, by blanchet
tuned proofs;
2012-03-19, by wenzelm
explicit propagation of assignment event, even if changed command set is empty;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
modernized axiomatizations;
2012-03-19, by wenzelm
updated Misc_Legacy.freeze_thaw;
2012-03-19, by wenzelm
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
2012-03-19, by wenzelm
moved some legacy stuff;
2012-03-19, by wenzelm
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
2012-03-19, by wenzelm
merged
2012-03-19, by wenzelm
merged
2012-03-19, by paulson
More structured proofs for cardinalities
2012-03-19, by paulson
merged
2012-03-19, by paulson
more structured case and induction proofs
2012-03-16, by paulson
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
2012-03-19, by blanchet
allow keyword tags to be redefined, but not the command category;
2012-03-19, by wenzelm
further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;
2012-03-19, by wenzelm
clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-19, by wenzelm
more robust bash interpolation;
2012-03-18, by wenzelm
more ambitious scalac options for makedist;
2012-03-18, by wenzelm
less noisy Isabelle/Scala build process;
2012-03-18, by wenzelm
comment;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-18, by wenzelm
tuned;
2012-03-18, by wenzelm
tuned structure;
2012-03-18, by wenzelm
comments for uniformity
2012-03-18, by haftmann
proper naming of simprocs according to actual target context;
2012-03-17, by wenzelm
amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
2012-03-17, by wenzelm
more precise syntax;
2012-03-17, by wenzelm
more antiquotations;
2012-03-17, by wenzelm
misc tuning to accomodate scala-2.10.0-M2;
2012-03-17, by wenzelm
include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;
2012-03-17, by wenzelm
merged
2012-03-17, by wenzelm
merged
2012-03-17, by paulson
tidying and structured proofs
2012-03-17, by paulson
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
simultaneous read_fields -- e.g. relevant for sort assignment;
2012-03-17, by wenzelm
added Syntax.read_typs;
2012-03-17, by wenzelm
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
2012-03-17, by wenzelm
tuned message;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
tuned proofs;
2012-03-17, by wenzelm
tuned exception;
2012-03-17, by wenzelm
merged;
2012-03-17, by wenzelm
spelt out missing colemmas
2012-03-17, by haftmann
generalized INF_INT_eq, SUP_UN_eq
2012-03-17, by haftmann
tuned specifications
2012-03-16, by haftmann
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
2012-03-17, by wenzelm
tuned grouping -- merely indicate order of magnitude;
2012-03-17, by wenzelm
slightly more parallel find_theorems;
2012-03-17, by wenzelm
'definition' no longer exports the foundational "raw_def";
2012-03-17, by wenzelm
some attempts to fit source on screen;
2012-03-17, by wenzelm
eliminated odd 'finalconsts' / Theory.add_finals;
2012-03-16, by wenzelm
modernized axiomatization;
2012-03-16, by wenzelm
modernized axiomatization;
2012-03-16, by wenzelm
afford strict Args.type_name (cf. 29e88714ffe4);
2012-03-16, by wenzelm
check declared vs. defined commands at end of session;
2012-03-16, by wenzelm
more abstract heading level;
2012-03-16, by wenzelm
less redundant data;
2012-03-16, by wenzelm
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
2012-03-16, by wenzelm
merged
2012-03-16, by wenzelm
ZF news
2012-03-16, by paulson
merged
2012-03-16, by paulson
Structured transfinite induction proofs
2012-03-16, by paulson
make more word theorems respect int/bin distinction
2012-03-16, by huffman
outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16, by wenzelm
refute_params are given in *this* theory;
2012-03-16, by wenzelm
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-16, by wenzelm
define keywords early when processing the theory header, before running the body commands;
2012-03-16, by wenzelm
clarified Keyword.is_keyword: union of minor and major;
2012-03-16, by wenzelm
Isabelle/jEdit supports user-defined Isar commands within the running session;
2012-03-15, by wenzelm
merged
2012-03-15, by wenzelm
beautification and structured proofs
2012-03-15, by paulson
replacing ":" by "\<in>"
2012-03-15, by paulson
Rewrote some induction proofs to be structured
2012-03-15, by paulson
more precise TPTP keywords and dependencies;
2012-03-15, by wenzelm
declare command keywords via theory header, including strict checking outside Pure;
2012-03-15, by wenzelm
prefer formally checked @{keyword} parser;
2012-03-15, by wenzelm
added ML antiquotation @{keyword};
2012-03-15, by wenzelm
declare minor keywords via theory header;
2012-03-15, by wenzelm
more explicit header_edits before main text_edits;
2012-03-15, by wenzelm
declare keywords as side-effect of header edit;
2012-03-15, by wenzelm
more recent recent_syntax, e.g. relevant for document rendering during startup;
2012-03-15, by wenzelm
clarified syntax of prospective keywords;
2012-03-15, by wenzelm
basic support for outer syntax keywords in theory header;
2012-03-15, by wenzelm
maintain Version.syntax within document state;
2012-03-15, by wenzelm
explicit Outer_Syntax.Decl;
2012-03-15, by wenzelm
allow multiple 'keywords' as in 'fixes';
2012-03-15, by wenzelm
some support for outer syntax keyword declarations within theory header;
2012-03-15, by wenzelm
merged
2012-03-14, by wenzelm
merged
2012-03-14, by paulson
structured case and induct rules
2012-03-14, by paulson
rudimentary documentation test
2012-03-14, by haftmann
doc-src build option (for emerging mira configuration)
2012-03-14, by haftmann
corrected fragile proof; tuned semicolons
2012-03-14, by haftmann
rudimentary distribution build configuration
2012-03-14, by haftmann
support for non-HTTP repository locations (important for mira); quasi-hardwired repository name
2012-03-14, by haftmann
corrected slip
2012-03-14, by haftmann
merged
2012-03-14, by paulson
rationalising the induction rule trans_induct3
2012-03-14, by paulson
allow modification of REPOS_NAME and REPOS from outside
2012-03-14, by haftmann
locale expressions without source positions;
2012-03-14, by wenzelm
tuned;
2012-03-14, by wenzelm
tuned messages;
2012-03-14, by wenzelm
source positions for locale and class expressions;
2012-03-14, by wenzelm
some proof indentation;
2012-03-14, by wenzelm
more explicit indication of swing thread context;
2012-03-14, by wenzelm
more indentation;
2012-03-14, by wenzelm
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
2012-03-14, by wenzelm
eliminated obsolete sanitize_name;
2012-03-14, by wenzelm
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
2012-03-14, by wenzelm
more parallel inductive_cases;
2012-03-14, by wenzelm
misc tuning;
2012-03-14, by wenzelm
updated to jedit_build-20120313 with jedit-4.5.0;
2012-03-13, by wenzelm
tuned context specifications and proofs;
2012-03-13, by wenzelm
tuned proofs;
2012-03-13, by wenzelm
clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-13, by wenzelm
more explicit indication of def names;
2012-03-13, by wenzelm
merged
2012-03-13, by paulson
Structured proofs concerning the square of an infinite cardinal
2012-03-13, by paulson
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
improved attribute "abs_def" to handle object-equality as well;
2012-03-13, by wenzelm
merged
2012-03-13, by wenzelm
More structured proofs about cardinal arithmetic
2012-03-13, by paulson
tuned proofs;
2012-03-13, by wenzelm
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-13, by wenzelm
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-03-13, by wenzelm
proper printing of empty binding (again, cf. 93f6f24010c2);
2012-03-13, by wenzelm
tuned;
2012-03-13, by wenzelm
tuned strip_alls;
2012-03-13, by wenzelm
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
2012-03-13, by wenzelm
some grouping of Par_List operations, to adjust granularity;
2012-03-12, by wenzelm
Par_List.map is already smart;
2012-03-12, by wenzelm
some support for grouped list operations;
2012-03-12, by wenzelm
merged;
2012-03-12, by wenzelm
merged
2012-03-12, by noschinl
NEWS
2012-03-12, by noschinl
use eventually_elim method
2012-03-12, by noschinl
add eventually_elim method
2012-03-12, by noschinl
merged
2012-03-12, by noschinl
tuned proofs
2012-03-12, by noschinl
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12, by noschinl
tuned simpset
2012-03-12, by noschinl
activate_notes in parallel -- to speedup main operation of locale interpretation;
2012-03-12, by wenzelm
refined activate_notes: simultaneous transformation before activation;
2012-03-12, by wenzelm
tuned headers;
2012-03-12, by wenzelm
merged
2012-03-12, by paulson
Structured proofs in ZF
2012-03-12, by paulson
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
2012-03-12, by wenzelm
updated polyml/build option to prefer included libffi;
2012-03-12, by wenzelm
tuned signature;
2012-03-12, by wenzelm
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
2012-03-12, by wenzelm
merged
2012-03-11, by wenzelm
renewing Executable_Relation
2012-03-11, by bulwahn
tuned;
2012-03-11, by wenzelm
more direct Name_Space.defined_entry;
2012-03-11, by wenzelm
eliminated old-fashioned 'constrains' element;
2012-03-11, by wenzelm
modernized locale expression, with some fluctuation of arguments;
2012-03-11, by wenzelm
simplified span class in conformance to Scala version;
2012-03-10, by wenzelm
discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
2012-03-10, by wenzelm
merged
2012-03-10, by wenzelm
adding tags to quickcheck's result
2012-03-10, by bulwahn
clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval;
2012-03-10, by wenzelm
eliminated dead code;
2012-03-10, by wenzelm
clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;
2012-03-10, by wenzelm
misc tuning and simplification;
2012-03-10, by wenzelm
tuned;
2012-03-10, by wenzelm
clarified Pattern.matchess;
2012-03-10, by wenzelm
tuned;
2012-03-10, by wenzelm
more precise alignment of begin/end, proof/qed;
2012-03-10, by wenzelm
merged
2012-03-09, by wenzelm
beautified
2012-03-09, by haftmann
more precise checking for wellformedness of mapper, before and after morphism application
2012-03-09, by haftmann
reject mapper terms with type variables not contained in the term's type
2012-03-09, by haftmann
always bracket case expressions in Scala
2012-03-09, by haftmann
tuned signature;
2012-03-09, by wenzelm
merges
2012-03-09, by paulson
More calculation-based cardinality proofs
2012-03-09, by paulson
split make_tptp_parser into two scripts, for parser and lib respectively;
2012-03-09, by sultana
added ml-yacc library sources;
2012-03-09, by sultana
added tptp parser;
2012-03-09, by sultana
merged
2012-03-08, by wenzelm
Structured and calculation-based proofs (with new trans rules!)
2012-03-08, by paulson
Structured and calculation-based proofs (with new trans rules!)
2012-03-08, by paulson
tuned comment;
2012-03-08, by wenzelm
simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2012-03-08, by wenzelm
tuned;
2012-03-08, by wenzelm
clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
2012-03-08, by wenzelm
more precise warning/error positions;
2012-03-08, by wenzelm
merged
2012-03-07, by wenzelm
less rigorous but more realistic migration recommendation; note on code generation of sets
2012-03-07, by haftmann
tuned syntax; more candidates
2012-03-07, by haftmann
tuned message (cf. ML version);
2012-03-07, by wenzelm
eliminated dead code;
2012-03-07, by wenzelm
tuned signature;
2012-03-07, by wenzelm
simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);
2012-03-07, by wenzelm
to_pred/set attributes now properly handle variables of type "... => T set"
2012-03-07, by berghofe
some recovery of IsaMakefile targets from f3c10e908f65;
2012-03-07, by wenzelm
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
2012-03-07, by sultana
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
2012-03-07, by sultana
added Mirabelle action info in its log file; tuned;
2012-03-07, by sultana
More mathematical symbols for ZF examples
2012-03-06, by paulson
mathematical symbols for Isabelle/ZF example theories
2012-03-06, by paulson
Using mathematical notation for <-> and cardinal arithmetic
2012-03-06, by paulson
mathematical symbols instead of ASCII
2012-03-06, by paulson
addressed a quotient-type-related issue that arose with the port to "set"
2012-03-04, by blanchet
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
2012-03-04, by blanchet
updates for jedit-4.5.0 (still inactive);
2012-03-04, by wenzelm
more explicit patches;
2012-03-04, by wenzelm
tuned comment;
2012-03-04, by wenzelm
removed obsolete proper_command_at (cf. 03a2dc9e0624);
2012-03-04, by wenzelm
added Command.proper_range (still unused);
2012-03-04, by wenzelm
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
2012-03-04, by wenzelm
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
2012-03-04, by wenzelm
tuned
2012-03-04, by haftmann
move test targets to test target
2012-03-04, by haftmann
dropped images for importer sessions
2012-03-04, by haftmann
dropped dead code
2012-03-04, by haftmann
more accurate dependencies
2012-03-04, by haftmann
tuned ML
2012-03-04, by haftmann
dropped silly code
2012-03-04, by haftmann
tuned
2012-03-04, by haftmann
dropped dead code
2012-03-04, by haftmann
actually add "the" Importer theory
2012-03-04, by haftmann
avoid internal hol4 name references in generic importer code
2012-03-04, by haftmann
generalized user-visible text
2012-03-03, by haftmann
generalized attribute name
2012-03-03, by haftmann
dropped dead theories
2012-03-03, by haftmann
one unified Importer theory
2012-03-03, by haftmann
added actual dependencies
2012-03-03, by haftmann
import all importer theories in compatibility layer
2012-03-03, by haftmann
merged;
2012-03-03, by wenzelm
dropped obsolete ROOT.ML
2012-03-03, by haftmann
plugged in pre-existing theories appropriately
2012-03-03, by haftmann
switch of target Import-HOL_Light-Imported: not operative at the moment
2012-03-03, by haftmann
turn on quick and dirty in batch mode
2012-03-03, by haftmann
tuned whitespace
2012-03-03, by haftmann
file system structure separating HOL4 and HOL Light concerns
2012-03-03, by haftmann
distribution of compatibility theories
2012-03-03, by haftmann
formal infrastructure for import sessions
2012-03-03, by haftmann
dropped dead code
2012-03-03, by haftmann
tuned whitespace
2012-03-03, by haftmann
spurious set/pred correction
2012-03-03, by haftmann
explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction
2012-03-03, by haftmann
explicit locations for import_theory and setup_theory, for better user interface conformance
2012-03-03, by haftmann
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
canonical argument order for attribute application;
2012-03-03, by wenzelm
clarified terminology of raw protocol messages;
2012-03-03, by wenzelm
tuned;
2012-03-03, by wenzelm
tuned signature -- emphasize Isabelle_Process Input vs. Output;
2012-03-03, by wenzelm
explicit syslog_limit reduces danger of low-level message flooding;
2012-03-03, by wenzelm
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
2012-03-03, by wenzelm
clarified scope of exception handlers;
2012-03-03, by wenzelm
relevant timing as in ML;
2012-03-03, by wenzelm
more fundamental pred-to-set conversions for range and domain by means of inductive_set
2012-03-02, by haftmann
merged
2012-03-02, by wenzelm
tuned whitespace
2012-03-02, by haftmann
tuned import
2012-03-02, by haftmann
dropped dead code
2012-03-02, by haftmann
terminate after first exception -- avoid syslog flooding;
2012-03-02, by wenzelm
avoid buffer loading overrun;
2012-03-02, by wenzelm
merged
2012-03-02, by wenzelm
collecting all axioms in a locale context in quickcheck;
2012-03-02, by bulwahn
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-03-02, by bulwahn
removing finiteness goals
2012-03-02, by bulwahn
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2012-03-02, by bulwahn
Symbol.encode header edits;
2012-03-01, by wenzelm
merged
2012-03-01, by wenzelm
tuned whitespace
2012-03-01, by haftmann
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-03-01, by haftmann
Removal of obsolete ML bindings
2012-03-01, by paulson
more robust locking;
2012-03-01, by wenzelm
proper update_header;
2012-03-01, by wenzelm
refined node_header -- more direct buffer access (again);
2012-03-01, by wenzelm
merged
2012-03-01, by wenzelm
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
2012-03-01, by blanchet
fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
2012-03-01, by blanchet
more robust set element extractor
2012-03-01, by blanchet
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
2012-03-01, by boehmes
tuned proofs;
2012-03-01, by wenzelm
more tolerant cygpath invocation, allow empty CLASSPATH;
2012-03-01, by wenzelm
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
2012-03-01, by wenzelm
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
2012-03-01, by wenzelm
more defensive node_header;
2012-02-29, by wenzelm
clarified module Thy_Load;
2012-02-29, by wenzelm
SMT fails if the chosen SMT solver is not installed
2012-02-29, by boehmes
merged
2012-02-28, by wenzelm
speed up Sledgehammer's clasimpset lookup a bit
2012-02-28, by blanchet
use SPASS instead of E for Metis examples -- it's seems faster for these small problems
2012-02-28, by blanchet
spelling
2012-02-28, by blanchet
avoid undeclared variables in let bindings;
2012-02-28, by wenzelm
tuned proofs;
2012-02-28, by wenzelm
more release tests;
2012-02-28, by wenzelm
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-28, by wenzelm
Finish localizing the quotient package.
2012-02-28, by Cezary Kaliszyk
merged
2012-02-28, by berghofe
Added infrastructure for mapping SPARK field / constructor names
2012-02-28, by berghofe
Use long prefix rather than short package name to disambiguate constant names
2012-02-27, by berghofe
more explicit development graph;
2012-02-27, by wenzelm
removed dead code (cf. a34d89ce6097);
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
removed introiff (cf. b09afce1e54f);
2012-02-27, by wenzelm
tuned;
2012-02-27, by wenzelm
removed broken/unused introiff (cf. d452117ba564);
2012-02-27, by wenzelm
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
2012-02-27, by wenzelm
tuned;
2012-02-27, by wenzelm
tuned proofs;
2012-02-27, by wenzelm
prefer uniform Timing.message -- avoid assumption about sequential execution;
2012-02-27, by wenzelm
prefer final ADTs -- prevent ooddities;
2012-02-27, by wenzelm
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-02-27, by wenzelm
more standard settings -- refer to COMPONENT at most once;
2012-02-27, by wenzelm
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
2012-02-27, by wenzelm
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-02-27, by wenzelm
eliminated odd comment from distant past;
2012-02-27, by wenzelm
updated cut_tac, without loose references to implementation manual;
2012-02-27, by wenzelm
updated generated file;
2012-02-27, by wenzelm
simplified cut_tac (cf. d549b5b0f344);
2012-02-27, by wenzelm
merged
2012-02-27, by huffman
avoid using constant Int.neg
2012-02-27, by huffman
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
2012-02-27, by wenzelm
merged
2012-02-27, by nipkow
added lemma
2012-02-27, by nipkow
converting "set [...]" to "{...}" in evaluation results
2012-02-27, by nipkow
removing Find_Unused_Assms_Examples from session as it requires much time
2012-02-27, by bulwahn
restored accidental omission
2012-02-26, by haftmann
dropped dead code
2012-02-26, by haftmann
tuned structure
2012-02-26, by haftmann
retain syntax here
2012-02-26, by haftmann
tuned structure; dropped already existing syntax declarations
2012-02-26, by haftmann
tuned syntax declarations; tuned structure
2012-02-26, by haftmann
merged
2012-02-26, by wenzelm
marked candidates for rule declarations
2012-02-26, by haftmann
include warning messages in node status;
2012-02-26, by wenzelm
tuned signature (in accordance with ML);
2012-02-26, by wenzelm
more PIDE modules;
2012-02-26, by wenzelm
tuned proofs;
2012-02-26, by wenzelm
more abstract class Document.State;
2012-02-26, by wenzelm
more abstract class Document.State.Assignment;
2012-02-26, by wenzelm
tuned signature;
2012-02-26, by wenzelm
more abstract class Document.Version;
2012-02-26, by wenzelm
more abstract class Document.Node;
2012-02-26, by wenzelm
more abstract class Document.History;
2012-02-26, by wenzelm
more abstract class Document.Change;
2012-02-26, by wenzelm
tuned;
2012-02-26, by wenzelm
tuned signature;
2012-02-26, by wenzelm
merged
2012-02-25, by wenzelm
slightly changing the enumeration scheme
2012-02-25, by bulwahn
adding some more test invocations of find_unused_assms
2012-02-25, by bulwahn
adding an example where random beats exhaustive testing
2012-02-25, by bulwahn
removing unnecessary assumptions in RComplete;
2012-02-25, by bulwahn
removing unnecessary assumptions in RealDef;
2012-02-25, by bulwahn
one general list_all2_update_cong instead of two special ones
2012-02-25, by bulwahn
tuned comments;
2012-02-25, by wenzelm
standard Graph instances;
2012-02-25, by wenzelm
clarified signature -- avoid oddities of Iterable like Iterator.map;
2012-02-25, by wenzelm
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
2012-02-25, by wenzelm
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
explicit is better than implicit
2012-02-24, by haftmann
dropped dead code
2012-02-24, by haftmann
prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
2012-02-24, by wenzelm
tuned imports;
2012-02-24, by wenzelm
tuned signature;
2012-02-24, by wenzelm
discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);
2012-02-24, by wenzelm
merged
2012-02-24, by wenzelm
remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
2012-02-24, by huffman
avoid using Int.succ_def in proofs
2012-02-24, by huffman
avoid using Int.succ or Int.pred in proofs
2012-02-24, by huffman
avoid using BIT_simps in proofs;
2012-02-24, by huffman
avoid using BIT_simps in proofs
2012-02-24, by huffman
updated stats according to src/HOL/IsaMakefile;
2012-02-24, by wenzelm
more precise clean target;
2012-02-24, by wenzelm
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
2012-02-24, by wenzelm
avoid using Int.Pls_def in proofs
2012-02-24, by huffman
remove ill-formed lemmas word_pred_0_Min and word_m1_Min
2012-02-24, by huffman
remove ill-formed lemma of_bl_no; adapt proofs
2012-02-24, by huffman
adapt lemma mask_lem to respect int/bin distinction
2012-02-24, by huffman
rephrase some slow "metis" calls
2012-02-24, by blanchet
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24, by blanchet
general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
2012-02-24, by blanchet
renamed 'try_methods' to 'try0'
2012-02-24, by blanchet
doc fixes (thanks to Nik)
2012-02-24, by blanchet
fixed arity bug with "If" helpers for "If" that returns a function
2012-02-24, by blanchet
given up disfruitful branch
2012-02-24, by haftmann
explicit remove of lattice notation
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24, by haftmann
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23, by haftmann
dropped dead code
2012-02-23, by haftmann
tuned isatest settings;
2012-02-23, by wenzelm
merged
2012-02-23, by wenzelm
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-23, by haftmann
tuned whitespace
2012-02-23, by haftmann
tuned proof
2012-02-23, by haftmann
prefer actual syntax categories;
2012-02-23, by wenzelm
avoid trait Addable, which is deprecated in scala-2.9.x;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype;
2012-02-23, by wenzelm
tuned -- avoid copy of empty value;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
streamlined abstract datatype, eliminating odd representation class;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
merged
2012-02-23, by huffman
make more simp rules respect int/bin distinction
2012-02-23, by huffman
make bool list functions respect int/bin distinction
2012-02-23, by huffman
merged;
2012-02-23, by wenzelm
tuned;
2012-02-23, by wenzelm
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2012-02-23, by wenzelm
further graph operations from ML;
2012-02-23, by wenzelm
removed dead code;
2012-02-23, by wenzelm
directed graphs (in Scala);
2012-02-23, by wenzelm
make uses of bin_split respect int/bin distinction
2012-02-23, by huffman
remove lemma bin_cat_Pls, which doesn't respect int/bin distinction
2012-02-23, by huffman
make uses of constant bin_sc respect int/bin distinction
2012-02-23, by huffman
remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc
2012-02-23, by huffman
remove unused lemmas
2012-02-23, by huffman
simplify proofs
2012-02-23, by huffman
make uses of bin_sign respect int/bin distinction
2012-02-23, by huffman
removed unnecessary lemma zero_bintrunc
2012-02-23, by huffman
remove unnecessary lemmas
2012-02-23, by huffman
removed unnecessary constant bin_rl
2012-02-23, by huffman
remove duplication of lemmas bin_{rest,last}_BIT
2012-02-23, by huffman
remove lemmas Bit{0,1}_div2
2012-02-23, by huffman
simplify proof
2012-02-23, by huffman
deal with FIXMEs for linarith examples
2012-02-23, by huffman
CONTRIBUTORS
2012-02-23, by haftmann
merged
2012-02-22, by huffman
tuned whitespace
2012-02-22, by huffman
tuned whitespace
2012-02-22, by huffman
adding documentation about find_unused_assms command and use_subtype option in the IsarRef
2012-02-22, by bulwahn
NEWS
2012-02-22, by bulwahn
adding some examples with find_unused_assms command
2012-02-22, by bulwahn
adding new command "find_unused_assms"
2012-02-22, by bulwahn
removing some unnecessary premises from Map theory
2012-02-22, by bulwahn
preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
2012-02-22, by bulwahn
generalizing inj_on_Int
2012-02-22, by bulwahn
moving Quickcheck's example to its own session
2012-02-22, by bulwahn
tuned proofs;
2012-02-21, by wenzelm
more robust visible_range: allow empty view;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
merged;
2012-02-21, by wenzelm
made SML/NJ happy;
2012-02-21, by wenzelm
tuned proofs;
2012-02-21, by wenzelm
merged
2012-02-21, by wenzelm
tuned proofs;
2012-02-21, by wenzelm
approximate Perspective.full within the bounds of the JVM;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
invoke later to reduce chance of causing deadlock;
2012-02-21, by wenzelm
misc tuning;
2012-02-21, by wenzelm
separate module for text status overview;
2012-02-21, by wenzelm
overview.delay_repaint: avoid wasting GUI cycles via update_delay;
2012-02-21, by wenzelm
tuned;
2012-02-21, by wenzelm
merged
2012-02-21, by berghofe
merged
2012-02-21, by berghofe
Fixed bugs:
2012-02-20, by berghofe
merged
2012-02-21, by bulwahn
subtype preprocessing in Quickcheck;
2012-02-21, by bulwahn
adding parsing of an optional predicate with quickcheck_generator command
2012-02-21, by bulwahn
updated generated files (cf. 8d51b375e926);
2012-02-21, by wenzelm
merged;
2012-02-21, by wenzelm
add missing lemmas to compute_div_mod
2012-02-21, by huffman
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
2012-02-21, by huffman
avoid using constant Int.neg
2012-02-21, by huffman
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
2012-02-21, by huffman
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-21, by haftmann
tuned whitespace
2012-02-20, by haftmann
tuned proof
2012-02-20, by haftmann
tuned proof
2012-02-19, by haftmann
distributed lattice properties of predicates to places of instantiation
2012-02-19, by haftmann
removing some unnecessary premises from Divides
2012-02-20, by bulwahn
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
2012-02-20, by huffman
observe HEIGHT of overview ticks;
2012-02-20, by wenzelm
more careful painting of overview component: more precise and more efficient;
2012-02-20, by wenzelm
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
2012-02-20, by wenzelm
use qualified constant names instead of suffixes (from Florian Haftmann)
2012-02-20, by huffman
tuned proofs
2012-02-18, by haftmann
tuned
2012-02-12, by haftmann
brute-force adjustion
2012-02-11, by haftmann
tuned whitespace
2012-02-11, by haftmann
tuned
2012-02-11, by haftmann
tuned
2012-02-10, by haftmann
tuned code
2012-02-10, by haftmann
dropped whitespace
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
corrected typo
2012-02-10, by haftmann
dropped dead code
2012-02-10, by haftmann
notepad is more appropriate here
2012-02-12, by haftmann
corrected treatment of applications of built-in functions to higher-order terms
2012-02-18, by boehmes
NEWS
2012-02-18, by krauss
merged
2012-02-18, by krauss
added congruence rules for Option.{map|bind}
2012-02-18, by krauss
updated generated documents
2012-02-18, by haftmann
avoid redefinition of @{theory} antiquotation
2012-02-18, by haftmann
update of generated documents
2012-02-18, by haftmann
tuned whitespace
2012-02-18, by haftmann
clarified
2012-02-18, by haftmann
corrected spelling
2012-02-18, by haftmann
clarified
2012-02-18, by haftmann
more precise semantics of "theory" antiquotation
2012-02-18, by haftmann
tuned import
2012-02-18, by haftmann
dropped references to obsolete theories
2012-02-18, by haftmann
adjusted to set type constructor
2012-02-18, by haftmann
tuned whitespace
2012-02-18, by haftmann
more explicit error on malformed abstract equation; dropped dead code; tuned signature
2012-02-18, by haftmann
simplified configuration options for syntax ambiguity;
2012-02-17, by wenzelm
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
2012-02-17, by wenzelm
more antiquotations;
2012-02-16, by wenzelm
more symbols;
2012-02-16, by wenzelm
tuned imports;
2012-02-16, by wenzelm
tuned proofs;
2012-02-16, by wenzelm
simplified configuration options for syntax ambiguity;
2012-02-16, by wenzelm
merged
2012-02-16, by wenzelm
removing unnecessary premise from diff_single_insert
2012-02-16, by bulwahn
explicit is better than implicit;
2012-02-16, by wenzelm
more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);
2012-02-16, by wenzelm
simplifying proof
2012-02-16, by bulwahn
removing unnecessary premises in theorems of List theory
2012-02-16, by bulwahn
tuning mutabelle script
2012-02-16, by bulwahn
adding documentation for abort_potential option in quickcheck
2012-02-16, by bulwahn
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-15, by wenzelm
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
2012-02-15, by wenzelm
uniform Isar source formatting for this file;
2012-02-15, by wenzelm
clarified outer syntax "constdecl", which is only local to some rail diagrams;
2012-02-15, by wenzelm
discontinued obsolete "prems" fact;
2012-02-15, by wenzelm
eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2012-02-15, by wenzelm
removed obsolete files;
2012-02-15, by wenzelm
more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);
2012-02-15, by wenzelm
removed dead code;
2012-02-15, by wenzelm
updated listrel (cf. 80dccedd6c14);
2012-02-15, by wenzelm
removed redundant cut_inst_tac -- already covered in implementation manual;
2012-02-15, by wenzelm
updated rewrite_goals_rule, rewrite_rule;
2012-02-15, by wenzelm
NEWS;
2012-02-15, by wenzelm
updated refs;
2012-02-15, by wenzelm
renamed "xstr" to "str_token";
2012-02-15, by wenzelm
merged
2012-02-14, by wenzelm
don't report spurious LEO-II errors
2012-02-14, by blanchet
better error message
2012-02-14, by blanchet
removing debug code in mutabelle
2012-02-14, by bulwahn
adding abort_potential functionality in quickcheck
2012-02-14, by bulwahn
adding abort_potential configuration in Quickcheck
2012-02-14, by bulwahn
clarified bires_inst_tac: retain internal exceptions;
2012-02-14, by wenzelm
tuned signature;
2012-02-14, by wenzelm
more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;
2012-02-14, by wenzelm
more conventional tactic setup;
2012-02-14, by wenzelm
eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
2012-02-14, by wenzelm
prefer high-level elim_format;
2012-02-14, by wenzelm
discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
2012-02-14, by wenzelm
method setup;
2012-02-14, by wenzelm
simplified use of tacticals;
2012-02-14, by wenzelm
comment;
2012-02-14, by wenzelm
tuned signature, according to actual usage of these operations;
2012-02-14, by wenzelm
tuned signature;
2012-02-14, by wenzelm
normalized aliases;
2012-02-14, by wenzelm
elininated unused INTLEAVE;
2012-02-14, by wenzelm
eliminated unused rewrite_goal_rule;
2012-02-14, by wenzelm
eliminated unused subgoals_tac;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
tuned;
2012-02-14, by wenzelm
merged, resolving trivial conflicts;
2012-02-14, by wenzelm
merged;
2012-02-14, by wenzelm
new SPASS options
2012-02-11, by blanchet
making num_mutations a configuration that can be changed with the mutabelle bash command
2012-02-11, by bulwahn
making max_mutants an option that can be changed in the Mutabelle-script
2012-02-11, by bulwahn
increase timeout to 30 seconds; changing mutabelle script
2012-02-11, by bulwahn
parse clauses generated from several formulas
2012-02-10, by blanchet
be more gentle when generating KBO weights
2012-02-10, by blanchet
update SPASS slices
2012-02-10, by blanchet
more specification of the quotient package in IsarRef
2012-02-10, by Cezary Kaliszyk
specification of the quotient package
2012-02-10, by Cezary Kaliszyk
tune KBO weight code
2012-02-09, by blanchet
minor DFG fix
2012-02-09, by blanchet
new SPASS slices
2012-02-09, by blanchet
improved KBO weights -- beware of explicit applications
2012-02-09, by blanchet
added possibility of generating KBO weights to DFG problems
2012-02-09, by blanchet
Generalize the compositional preservation theorems
2012-02-09, by Cezary Kaliszyk
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-02-08, by blanchet
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
2012-02-08, by blanchet
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
2012-02-08, by blanchet
fixed arity error
2012-02-06, by blanchet
tuning
2012-02-06, by blanchet
renamed type encoding
2012-02-06, by blanchet
adding some forbidden constant names for mutabelle
2012-02-05, by bulwahn
mutabelle ignores theorems with internal constants
2012-02-05, by bulwahn
tuned
2012-02-05, by nipkow
merged
2012-02-05, by nipkow
simplified code generation
2012-02-05, by nipkow
remove option that's on by default
2012-02-05, by blanchet
no need for a script/mega-hack with the new SPASS
2012-02-05, by blanchet
cleaned up new SPASS parsing
2012-02-05, by blanchet
tuning
2012-02-05, by blanchet
merged
2012-02-05, by bulwahn
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
2012-02-05, by bulwahn
tuning to remove ML warnings
2012-02-05, by bulwahn
removed double filtering of type args
2012-02-05, by blanchet
adding a quickcheck example about functions and sets
2012-02-05, by bulwahn
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
2012-02-05, by bulwahn
adding a remark about lemma which is too special and should be removed
2012-02-05, by bulwahn
another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-05, by bulwahn
beautifying definitions of check_all and adding instance for finite_4
2012-02-05, by bulwahn
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2012-02-05, by Cezary Kaliszyk
added option to Mirabelle/Sledgehammer
2012-02-04, by blanchet
improved hashing w.r.t. Mirabelle, to help debugging
2012-02-04, by blanchet
tuned SPASS DFG output
2012-02-04, by blanchet
the new SPASS gives accurate fact information, so no need for old hack anymore
2012-02-04, by blanchet
fixed docs
2012-02-04, by blanchet
made sure to filter type args also for "uncurried alias" equations
2012-02-04, by blanchet
made option available to users (mostly for experiments)
2012-02-04, by blanchet
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
2012-02-04, by bulwahn
optimization: slice caching in case two consecutive slices are nearly identical
2012-02-03, by blanchet
extended SPASS/DFG output with ranks
2012-02-03, by blanchet
try to pass fewer options to Metis
2012-02-03, by blanchet
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
2012-02-03, by Cezary Kaliszyk
improve SPASS scripts
2012-02-02, by blanchet
change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02, by blanchet
better SPASS setup
2012-02-02, by blanchet
don't introduce new symbols in helpers -- makes problems unprovable
2012-02-02, by blanchet
only constants can be aliased
2012-02-02, by blanchet
include new SPASS by default if available
2012-02-02, by blanchet
adding an example for finite and cofinite sets
2012-02-02, by bulwahn
adding a minimally refined equality on sets for code generation
2012-02-02, by bulwahn
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2012-02-02, by bulwahn
improving code equations for multisets that violated the distinct AList abstraction
2012-02-01, by bulwahn
tuning
2012-02-02, by blanchet
implemented partial application aliases (for SPASS mainly)
2012-02-02, by blanchet
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
2012-02-01, by blanchet
don't stumble on SPASS debug output
2012-02-01, by blanchet
tuning
2012-02-01, by blanchet
proper statuses for "fact_from_ref"
2012-02-01, by blanchet
tuned
2012-01-31, by nipkow
renamed Sledgehammer option
2012-01-31, by blanchet
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31, by blanchet
improve SPASS setup
2012-01-31, by blanchet
adding code equation for setsum
2012-01-31, by bulwahn
avoid name clash, really
2012-01-31, by blanchet
fixed syntax bug in DFG output
2012-01-31, by blanchet
new SPASS setup
2012-01-31, by blanchet
distinguish between ":lr" and ":lt" (terminating) in DFG format
2012-01-31, by blanchet
nicer keyword class avoidance scheme
2012-01-31, by blanchet
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
2012-01-31, by blanchet
mutabelle must handle the case where quickcheck returns multiple results
2012-01-31, by bulwahn
reverted e2b1a86d59fc -- broke Metis's lambda-lifting
2012-01-31, by blanchet
merged
2012-01-31, by nipkow
NEWS
2012-01-31, by nipkow
added "'a rel"
2012-01-30, by nipkow
fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
2012-01-30, by blanchet
new SPASS setup
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
implemented new lambda translations scheme
2012-01-30, by blanchet
avoid unsupported case in Metis
2012-01-30, by blanchet
docs and news
2012-01-30, by blanchet
rename lambda translation schemes
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
NEWS
2012-01-30, by bulwahn
renaming all lemmas with name rel_pow to relpow
2012-01-30, by bulwahn
adding code equations for max_extp and mlex
2012-01-30, by bulwahn
adding code generation for relpow by copying the ideas for code generation of funpow
2012-01-30, by bulwahn
adding code equation for rtranclp in Enum
2012-01-30, by bulwahn
adding code equation for max_ext
2012-01-30, by bulwahn
adding code equation for tranclp
2012-01-30, by bulwahn
adding code_unfold to make measure executable
2012-01-30, by bulwahn
removed accidental dependance of abstract interpreter on gamma
2012-01-29, by nipkow
merged
2012-01-29, by nipkow
tuned
2012-01-29, by nipkow
an executable version of accessible part (only for finite types yet)
2012-01-28, by bulwahn
adding yet another induction rule on natural numbers
2012-01-28, by bulwahn
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
2012-01-28, by bulwahn
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
2012-01-28, by bulwahn
adding some more examples for quickcheck; replaced FIXME comments
2012-01-27, by bulwahn
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
2012-01-27, by bulwahn
removed duplicate definitions that made locale inconsistent
2012-01-27, by nipkow
added parity analysis
2012-01-27, by nipkow
corrected expectation; added an example for quickcheck
2012-01-27, by bulwahn
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
2012-01-27, by bulwahn
made SML/NJ happy
2012-01-27, by blanchet
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
2012-01-26, by blanchet
separate orthogonal components
2012-01-26, by blanchet
generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
2012-01-26, by blanchet
better handling of individual type for DFG format (SPASS)
2012-01-26, by blanchet
adding quickcheck example with THE
2012-01-26, by bulwahn
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
2012-01-26, by bulwahn
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
2012-01-26, by bulwahn
tuned
2012-01-26, by nipkow
adding very basic code generation to Wellfounded theory
2012-01-25, by bulwahn
removing dead code from Mutabelle; tuned
2012-01-25, by bulwahn
generalizing check if size matters because it is different for random and exhaustive testing
2012-01-25, by bulwahn
merged
2012-01-25, by bulwahn
adding code equation for Collect on finite types
2012-01-25, by bulwahn
Use lookup_size rather than Datatype.get_info in is_poly to avoid
2012-01-24, by berghofe
adding some rules to quickcheck's preprocessing
2012-01-24, by bulwahn
some more constants on mutabelle's blacklist
2012-01-24, by bulwahn
implemented "tptp_refute" tool
2012-01-23, by blanchet
added problem importer
2012-01-23, by blanchet
imported patch ATP_Problem_Import.thy
2012-01-23, by blanchet
imported patch atp_problem_import.ML
2012-01-23, by blanchet
renamed theory exporter
2012-01-23, by blanchet
renamed two files to make room for a new file
2012-01-23, by blanchet
rebranded Nitrox, for more uniformity
2012-01-23, by blanchet
moved "nitrox" to TPTP
2012-01-23, by blanchet
generalize type of List.listrel
2012-01-23, by huffman
support for Ex1 in quickcheck-narrowing
2012-01-23, by bulwahn
adding another internal constant to mutabelle's blacklust
2012-01-23, by bulwahn
adding some more forbidden constant names for the mutated conjecture generation
2012-01-23, by bulwahn
adding code generation for some list relations
2012-01-23, by bulwahn
adding fun_eq_iff to the preprocessing
2012-01-23, by bulwahn
random instance for sets
2012-01-23, by bulwahn
more configurations to mutabelle
2012-01-23, by bulwahn
catching code generation errors in quickcheck-narrowing
2012-01-20, by bulwahn
adding narrowing instance for sets
2012-01-20, by bulwahn
shortened definitions by adding some termify constants
2012-01-20, by bulwahn
tuned
2012-01-20, by bulwahn
adding check_all instance for sets; tuned
2012-01-20, by bulwahn
tuned
2012-01-20, by nipkow
tuned
2012-01-20, by nipkow
minor edits in docs
2012-01-19, by blanchet
renamed "sound" option to "strict"
2012-01-19, by blanchet
updated Sledge docs some more
2012-01-19, by blanchet
more doc updates
2012-01-19, by blanchet
updated docs
2012-01-19, by blanchet
lower timeout for preplay, now that we have more preplay methods
2012-01-19, by blanchet
cleanly separate each Metis encoding
2012-01-19, by blanchet
basic setup for equational reasoning;
2012-02-09, by wenzelm
tuned;
2012-02-07, by wenzelm
updated examples for syntax translations;
2012-02-07, by wenzelm
updated section on raw syntax;
2012-02-05, by wenzelm
updated section about syntax ambiguity;
2012-02-05, by wenzelm
updated/unified section on mixfix annotations;
2012-02-04, by wenzelm
tuned;
2012-02-04, by wenzelm
more on explicit notation;
2012-02-04, by wenzelm
more accurate Pure grammar;
2012-02-04, by wenzelm
more refs;
2012-02-04, by wenzelm
simplified mixfix (NB: infix is no longer required separately);
2012-02-04, by wenzelm
updated section on print modes;
2012-02-02, by wenzelm
misc tuning and reformatting;
2012-02-02, by wenzelm
clarified syntax section structure;
2012-02-02, by wenzelm
discontinued obscure history commands;
2012-02-02, by wenzelm
misc tuning and reformatting;
2012-02-02, by wenzelm
discontinued obscure history commands;
2012-02-02, by wenzelm
updated hint about asm_rl;
2012-01-29, by wenzelm
updated thin_tac;
2012-01-29, by wenzelm
updated distinct_subgoals_tac, flexflex_tac;
2012-01-29, by wenzelm
removed obscure material;
2012-01-29, by wenzelm
updated rotate_tac;
2012-01-29, by wenzelm
tuned;
2012-01-27, by wenzelm
updated citations;
2012-01-27, by wenzelm
updated subgoal_tac;
2012-01-27, by wenzelm
tuned sectioning;
2012-01-26, by wenzelm
updated "Control and search tacticals" (moved from ref to implementation);
2012-01-26, by wenzelm
obsolete -- covered in implementation manual;
2012-01-26, by wenzelm
moved HEADGOAL;
2012-01-26, by wenzelm
removed some obscure material;
2012-01-26, by wenzelm
added SELECT_GOAL;
2012-01-26, by wenzelm
tuned;
2012-01-26, by wenzelm
updated "subgoal quantifiers";
2012-01-25, by wenzelm
tuned ML infixes;
2012-01-25, by wenzelm
document antiquotations for ML infix operators;
2012-01-25, by wenzelm
tuned;
2012-01-25, by wenzelm
updated repetition tacticals;
2012-01-25, by wenzelm
updated THEN, ORELSE, APPEND, and derivatives;
2012-01-25, by wenzelm
removed obscure/outdated material;
2012-01-25, by wenzelm
updated RSN, RL, RLN, MRS;
2012-01-25, by wenzelm
removed obscure/outdated material;
2012-01-25, by wenzelm
tuned;
2012-01-25, by wenzelm
more on Logic.all/mk_implies etc.;
2012-01-25, by wenzelm
reduce AFP test by many hours;
2012-01-19, by wenzelm
added termination of narrowing
2012-01-19, by nipkow
really need 64bit here;
2012-01-18, by wenzelm
Added termination proof for widening
2012-01-18, by nipkow
switch afp test to Darwin on macbroy2
2012-01-18, by kleing
merged
2012-01-18, by nipkow
introduced commands over a set of vars
2012-01-18, by nipkow
basic support for PIDE Scala programming, independently of the main Isabelle repository;
2012-01-18, by wenzelm
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
2012-01-17, by blanchet
updated message
2012-01-17, by blanchet
improve installation instructions
2012-01-17, by blanchet
allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script
2012-01-17, by blanchet
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
2012-01-17, by huffman
refreshing NEWS
2012-01-17, by bulwahn
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
2012-01-17, by bulwahn
renamed theory AList to DAList
2012-01-17, by bulwahn
position constraints for numerals enable PIDE markup;
2012-01-16, by wenzelm
more careful cumulation of tooltips -- ensure uniform range;
2012-01-16, by wenzelm
tuned;
2012-01-16, by wenzelm
tuned
2012-01-16, by nipkow
missing dependency
2012-01-16, by nipkow
tuned example;
2012-01-15, by wenzelm
merged
2012-01-15, by wenzelm
back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
2012-01-15, by wenzelm
recovered outdated_color (cf. 4beb2f41ed93);
2012-01-15, by wenzelm
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
2012-01-15, by wenzelm
tuned proofs;
2012-01-15, by wenzelm
tuned
2012-01-15, by nipkow
tuned signature;
2012-01-15, by wenzelm
comments;
2012-01-15, by wenzelm
tuned proofs;
2012-01-15, by wenzelm
eliminated dead code, together with spurious warning about congruence rule for "Fun.comp";
2012-01-15, by wenzelm
more explicit/robust treatment of common snapshot;
2012-01-15, by wenzelm
discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14, by wenzelm
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14, by wenzelm
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2012-01-14, by wenzelm
tuned;
2012-01-14, by wenzelm
discontinued old-style Term.list_all_free in favour of plain Logic.all;
2012-01-14, by wenzelm
tuned;
2012-01-14, by wenzelm
discontinued default rendering for Oheimb's double-space;
2012-01-14, by wenzelm
tuned white space;
2012-01-14, by wenzelm
tuned comment;
2012-01-14, by wenzelm
paranoia null check -- prevent spurious crash of jedit token markup;
2012-01-14, by wenzelm
tuned comments;
2012-01-14, by wenzelm
tuned signature;
2012-01-14, by wenzelm
clarified partial restrict operation;
2012-01-14, by wenzelm
tuned proofs;
2012-01-14, by wenzelm
ignore empty gfx_range;
2012-01-14, by wenzelm
tuned signature;
2012-01-14, by wenzelm
tuned
2012-01-13, by nipkow
handle specific exception, not arbitrary ones (including Interrupt);
2012-01-13, by wenzelm
eliminated dead code;
2012-01-13, by wenzelm
more modest settings for lxbroy10 -- might actually perform better;
2012-01-12, by wenzelm
tuned;
2012-01-12, by wenzelm
improved select_markup: include filtering of defined results;
2012-01-12, by wenzelm
tuned text_color: cumulate with explicit default color;
2012-01-12, by wenzelm
added cat_lines convenience;
2012-01-12, by wenzelm
tuned;
2012-01-12, by wenzelm
clarified mkString: no extra line-breaks for XML.Body;
2012-01-12, by wenzelm
adding exhaustive instances for type constructor set
2012-01-12, by bulwahn
Updated generated file
2012-01-12, by berghofe
Added inf_Int_eq to pred_set_conv database as well
2012-01-12, by berghofe
more conventional eval_tac vs. method_setup "eval";
2012-01-11, by wenzelm
updated generated file -- change of printed case syntax probably due to f805747f8571;
2012-01-11, by wenzelm
actually try to preserve names given by user (cf. 463b594e186a);
2012-01-11, by wenzelm
updated example -- List.foldl is no longer defined via primrec;
2012-01-11, by wenzelm
more qualified names;
2012-01-11, by wenzelm
refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;
2012-01-11, by wenzelm
more robust ISABELLE_HOME_USER for repository versions -- some versions of Emacs interpret foo//bar as /bar even on the command-line (unlike regular POSIX semantics);
2012-01-11, by wenzelm
merged
2012-01-11, by berghofe
Removed strange hack introduced in b27e93132603, since equivariance
2012-01-11, by berghofe
Replaced perm_set_eq by perm_set_def
2012-01-10, by berghofe
Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete
2012-01-10, by berghofe
Reverted several lemmas involving sets to the state before the
2012-01-10, by berghofe
clarified Isabelle_Rendering vs. physical painting;
2012-01-10, by wenzelm
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
2012-01-10, by berghofe
pred_subset/equals_eq are now standard pred_set_conv rules
2012-01-10, by berghofe
Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
2012-01-10, by berghofe
merged
2012-01-10, by huffman
add simp rules for set_bit and msb applied to 0 and 1
2012-01-10, by huffman
add simp rule test_bit_1
2012-01-10, by huffman
proper hiding of facts and constants in AList_Impl and AList theory
2012-01-10, by bulwahn
NEWS
2012-01-10, by bulwahn
adding quickcheck examples with multisets
2012-01-10, by bulwahn
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
2012-01-10, by bulwahn
adding theory association lists with invariant
2012-01-10, by bulwahn
command status color via regular markup;
2012-01-09, by wenzelm
proper cumulation of bulk arguments;
2012-01-09, by wenzelm
tuned;
2012-01-09, by wenzelm
merge
2012-01-09, by blanchet
revert unintended "sledgehammer" call
2012-01-09, by blanchet
prefer antiquotations;
2012-01-09, by wenzelm
misc tuning and reformatting;
2012-01-09, by wenzelm
updated generated file;
2012-01-09, by wenzelm
Added termination to IMP Abs_Int
2012-01-09, by nipkow
added lemmas
2012-01-09, by nipkow
massaging of code setup for sets
2012-01-07, by haftmann
dropped theory More_Set
2012-01-07, by haftmann
use Inf/Sup_bool_def/apply as code equations
2012-01-07, by haftmann
tuned
2012-01-07, by nipkow
accumulate status as regular markup for command range;
2012-01-07, by wenzelm
corrected slip
2012-01-07, by haftmann
tuned
2012-01-07, by haftmann
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
2012-01-07, by haftmann
moved lemmas about List.set and set operations to List theory
2012-01-06, by haftmann
moved lemmas about List.set and set operations to List theory
2012-01-06, by haftmann
incorporated various theorems from theory More_Set into corpus
2012-01-06, by haftmann
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
2012-01-06, by haftmann
merged
2012-01-06, by wenzelm
farewell to theory More_List
2012-01-06, by haftmann
dropped unused nth_map
2012-01-06, by haftmann
more explicit NEWS
2012-01-06, by haftmann
refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
2012-01-06, by wenzelm
tuned;
2012-01-06, by wenzelm
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
2012-01-06, by wenzelm
tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
2012-01-06, by wenzelm
recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);
2012-01-06, by wenzelm
more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
2012-01-06, by wenzelm
proper refs;
2012-01-06, by wenzelm
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
2012-01-06, by haftmann
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
2012-01-06, by haftmann
prefer listsum over foldl plus 0
2012-01-06, by haftmann
prefer concat over foldl append []
2012-01-06, by haftmann
tuned proofs
2012-01-06, by haftmann
interaction of set operations for execution and membership predicate
2012-01-01, by haftmann
cleanup of code declarations
2012-01-01, by haftmann
discontinued Syntax.positions -- atomic parse trees are always annotated;
2012-01-05, by wenzelm
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
2012-01-05, by wenzelm
misc tuning;
2012-01-05, by wenzelm
prefer raw_message for protocol implementation;
2012-01-05, by wenzelm
prefer raw_message for protocol implementation;
2012-01-05, by wenzelm
prefer raw_message for protocol implementation;
2012-01-05, by wenzelm
tuned signature;
2012-01-05, by wenzelm
tuned signature -- emphasize special nature of protocol commands;
2012-01-05, by wenzelm
updated version information;
2012-01-05, by wenzelm
updated version information;
2012-01-04, by wenzelm
generalised type
2012-01-04, by nipkow
improved "set" support by code inspection
2012-01-04, by blanchet
remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-04, by blanchet
tuning
2012-01-04, by blanchet
handle higher-order occurrences of sets gracefully in model display
2012-01-04, by blanchet
prefer explicit version information;
2012-01-04, by wenzelm
more Nitpick doc updates
2012-01-04, by blanchet
reenable Kodkodi in Mira now that Nitpick has been ported to 'a set constructor
2012-01-04, by blanchet
reenable Kodkodi in Isatest now that Nitpick has been ported to 'a set constructor
2012-01-04, by blanchet
fixed bisimilarity axiom -- avoid "insert" with wrong type
2012-01-03, by blanchet
tuning
2012-01-03, by blanchet
updated Nitpick docs after "set" reintroduction
2012-01-03, by blanchet
no abuse of notation
2012-01-03, by blanchet
always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
2012-01-03, by blanchet
more robust destruction of "set Collect" idiom
2012-01-03, by blanchet
handle starred predicates correctly w.r.t. "set"
2012-01-03, by blanchet
handle "Id" gracefully w.r.t. "set"
2012-01-03, by blanchet
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
2012-01-03, by blanchet
handle "set" correctly in Refute -- inspired by old code from Isabelle2007
2012-01-03, by blanchet
create consts with proper "set" types
2012-01-03, by blanchet
tuned Refute
2012-01-03, by blanchet
lower cardinality for faster testing
2012-01-03, by blanchet
simplify mem Collect
2012-01-03, by blanchet
tuning
2012-01-03, by blanchet
ported Minipick to "set"
2012-01-03, by blanchet
fixed set extensionality code
2012-01-03, by blanchet
tuned import
2012-01-03, by blanchet
construct correct "set" type for wf goal
2012-01-03, by blanchet
fixed Nitpick's typedef handling w.r.t. "set"
2012-01-03, by blanchet
fixed type annotations
2012-01-03, by blanchet
rationalized output (a bit)
2012-01-03, by blanchet
fixed a few more bugs in \Nitpick's new "set" support
2012-01-03, by blanchet
regenerate SMT example certificates, to reflect "set" type constructor
2012-01-03, by blanchet
port part of Nitpick to "set" type constructor
2012-01-03, by blanchet
reintroduced failing examples now that they work again, after reintroduction of "set"
2012-01-03, by blanchet
ported mono calculus to handle "set" type constructors
2012-01-03, by blanchet
fixed spurious catch-all patterns
2012-01-03, by blanchet
more benchmarks;
2012-01-03, by wenzelm
tuned
2012-01-02, by nipkow
ported "Sets" example to "set" type constructor
2012-01-02, by blanchet
ported a dozen of proofs to the "set" type constructor
2012-01-02, by blanchet
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
2012-01-02, by blanchet
update docs to reflect "Manual_Nits"
2012-01-02, by blanchet
removed special handling for set constants in relevance filter
2012-01-02, by blanchet
reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
2012-01-02, by blanchet
killed unfold_set_const option that makes no sense now that set is a type constructor again
2012-01-02, by blanchet
tuned
2012-01-02, by nipkow
removed unnecessary lemmas
2012-01-02, by nipkow
tuned proofs
2012-01-02, by nipkow
tuned var names
2012-01-01, by nipkow
tuned argument order
2012-01-01, by nipkow
merged
2012-01-01, by huffman
add simp rules for bitwise word operations with 1
2011-12-30, by huffman
tuned types
2011-12-31, by nipkow
disabled failing sledgehammer unit test (collateral damage of 184d36538e51)
2011-12-31, by krauss
disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)
2011-12-31, by krauss
merged
2011-12-30, by berghofe
Made gen_dest_case more robust against eta contraction
2011-12-30, by berghofe
merged
2011-12-30, by wenzelm
remove unnecessary intermediate lemmas
2011-12-30, by huffman
tuned;
2011-12-30, by wenzelm
eliminated old-fashioned Global_Theory.add_thms;
2011-12-30, by wenzelm
simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;
2011-12-30, by wenzelm
simplified proof;
2011-12-30, by wenzelm
simplified proof;
2011-12-30, by wenzelm
simplified proof;
2011-12-30, by wenzelm
more parallelism;
2011-12-30, by wenzelm
tuned;
2011-12-30, by wenzelm
merged
2011-12-29, by wenzelm
tuned -- afford slightly larger simpset in simp_defs_tac;
2011-12-29, by wenzelm
tuned -- standard proofs by default;
2011-12-29, by wenzelm
do not fork skipped proofs;
2011-12-29, by wenzelm
clarified timeit_msg;
2011-12-29, by wenzelm
tuned;
2011-12-29, by wenzelm
comments;
2011-12-29, by wenzelm
remove constant 'ccpo.lub', re-use constant 'Sup' instead
2011-12-29, by huffman
merged
2011-12-29, by nipkow
tuned
2011-12-29, by nipkow
conversions from sets to predicates and vice versa; extensionality on predicates
2011-12-29, by haftmann
added implementation of pred_of_set
2011-12-29, by haftmann
fundamental theorems on Set.bind
2011-12-29, by haftmann
updated generated files;
2011-12-29, by wenzelm
qualified Finite_Set.fold
2011-12-29, by haftmann
qualified Finite_Set.fold
2011-12-29, by haftmann
dropped redundant setup
2011-12-29, by haftmann
tuned declaration
2011-12-29, by haftmann
attribute code_abbrev superseedes code_unfold_post; tuned text
2011-12-29, by haftmann
attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
2011-12-29, by haftmann
attribute code_abbrev superseedes code_unfold_post
2011-12-29, by haftmann
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
2011-12-29, by haftmann
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-12-29, by haftmann
merged
2011-12-28, by wenzelm
merged
2011-12-28, by huffman
restate some lemmas to respect int/bin distinction
2011-12-28, by huffman
simplify some proofs
2011-12-28, by huffman
add lemma word_eq_iff
2011-12-28, by huffman
restate lemma word_1_no in terms of Numeral1
2011-12-28, by huffman
remove recursion combinator bin_rec;
2011-12-28, by huffman
simplify definition of XOR for type int;
2011-12-28, by huffman
simplify definition of OR for type int;
2011-12-28, by huffman
simplify definition of NOT for type int
2011-12-28, by huffman
add several new tests, most of which don't work yet
2011-12-28, by huffman
fix typos
2011-12-28, by huffman
remove some duplicate lemmas
2011-12-28, by huffman
simplify proof
2011-12-28, by huffman
replace 'lemmas' with explicit 'lemma'
2011-12-28, by huffman
add section headings
2011-12-28, by huffman
remove duplicate lemma lists
2011-12-27, by huffman
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
2011-12-28, by wenzelm
disable kodkodi for now to prevent isatest failure of HOL-Nitpick_Examples due to 'a set constructor;
2011-12-28, by wenzelm
updated platform information;
2011-12-28, by wenzelm
discontinued broken macbroy5 and thus the obsolete ppc-darwin platform;
2011-12-28, by wenzelm
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
2011-12-28, by wenzelm
print case syntax depending on "show_cases" configuration option;
2011-12-28, by wenzelm
merged
2011-12-27, by huffman
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
2011-12-27, by huffman
remove some uses of Int.succ and Int.pred
2011-12-27, by huffman
removed unused lemmas
2011-12-27, by huffman
remove redundant syntax declaration
2011-12-27, by huffman
use 'induct arbitrary' instead of 'rule_format' attribute
2011-12-27, by huffman
declare simp rules immediately, instead of using 'declare' commands
2011-12-27, by huffman
declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin
2011-12-27, by huffman
be explicit about Finite_Set.fold
2011-12-27, by haftmann
dropped fact whose names clash with corresponding facts on canonical fold
2011-12-27, by haftmann
prefer canonical fold on lists
2011-12-27, by haftmann
be explicit about Finite_Set.fold
2011-12-27, by haftmann
incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-12-26, by haftmann
moved theorem requiring multisets from More_List to Multiset
2011-12-26, by haftmann
NEWS: unavoidable fact renames
2011-12-26, by haftmann
dropped disfruitful `constant signatures`
2011-12-26, by haftmann
moved various set operations to theory Set (resp. Product_Type)
2011-12-26, by haftmann
dropped Executable_Set wrapper theory
2011-12-26, by haftmann
updated certificate
2011-12-25, by haftmann
NEWS: `set` is now a proper type constructor
2011-12-24, by haftmann
dropped references to obsolete facts `mem_def` and `Collect_def`
2011-12-24, by haftmann
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
2011-12-24, by haftmann
adjusted to set/pred distinction by means of type constructor `set`
2011-12-24, by haftmann
treatment of type constructor `set`
2011-12-24, by haftmann
executable intervals
2011-12-24, by haftmann
`set` is now a proper type constructor
2011-12-24, by haftmann
tuned layout
2011-12-24, by haftmann
reduced to a compatibility layer
2011-12-24, by haftmann
added setup for executable code
2011-12-24, by haftmann