isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle