isabelle: Graph

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