2011-09-25 ago wenzelm tuned signature;
2011-09-25 ago wenzelm more uniform defaults;
2011-09-25 ago haftmann Quotient_Set.thy is part of library
2011-09-25 ago nipkow fixed typo
2011-09-24 ago wenzelm standardize drive letters -- important for proper document node identification;
2011-09-24 ago wenzelm more user aliases;
2011-09-24 ago sultana fixed IsaMakefile action for HOL-TPTP.
2011-09-23 ago wenzelm prefer socket comminication on Cygwin, which is more stable here than fifos;
2011-09-23 ago wenzelm tuned proof;
2011-09-23 ago wenzelm made SML/NJ happy;
2011-09-23 ago wenzelm discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
2011-09-23 ago wenzelm updated header;
2011-09-23 ago wenzelm merged;
2011-09-23 ago blanchet reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
2011-09-23 ago blanchet first step towards extending Minipick with more translations
2011-09-23 ago berghofe Include keywords print_coercions and print_coercion_maps
2011-08-17 ago traytel local coercion insertion algorithm to support complex coercions
2011-08-17 ago traytel printing and deleting of coercions
2011-09-23 ago wenzelm raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
2011-09-23 ago wenzelm default print mode for Isabelle/Scala, not just Isabelle/jEdit;
2011-09-23 ago wenzelm augment existing print mode;
2011-09-23 ago wenzelm explicit option for socket vs. fifo communication;
2011-09-23 ago wenzelm tuned proof;
2011-09-23 ago blanchet synchronized section names with manual
2011-09-23 ago wenzelm merged;
2011-09-22 ago huffman discontinued legacy theorem names from RealDef.thy
2011-09-22 ago huffman merged
2011-09-22 ago huffman discontinued HOLCF legacy theorem names
2011-09-22 ago blanchet take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
2011-09-22 ago berghofe Moved extraction part of Higman's lemma to separate theory to allow reuse in
2011-09-22 ago berghofe Removed hcentering and vcentering options, since they are not supported
2011-09-22 ago berghofe merged
2011-09-22 ago berghofe Added documentation for HOL-SPARK
2011-09-22 ago blanchet drop partial monomorphic instances in Metis, like in Sledgehammer
2011-09-22 ago blanchet better type reconstruction -- prevents ill-instantiations in proof replay
2011-09-22 ago hoelzl NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-22 ago bulwahn changing quickcheck_timeout to 30 seconds in mutabelle's testing
2011-09-22 ago bulwahn adding post-processing of terms to narrowing-based Quickcheck
2011-09-21 ago huffman HOL/ex/ROOT.ML: only list BinEx once
2011-09-21 ago huffman merged
2011-09-21 ago huffman remove redundant instantiation ereal :: power
2011-09-21 ago blanchet reintroduced Minipick as Nitpick example
2011-09-21 ago blanchet tuned comment
2011-09-21 ago huffman merged
2011-09-20 ago huffman Extended_Real_Limits: generalize some lemmas
2011-09-20 ago huffman add lemmas within_empty and tendsto_bot;
2011-09-22 ago wenzelm made SML/NJ happy;
2011-09-22 ago wenzelm abstract System_Channel in ML (cf. Scala version);
2011-09-21 ago wenzelm alternative Socket_Channel;
2011-09-21 ago wenzelm more abstract wrapping of fifos as System_Channel;
2011-09-21 ago wenzelm slightly more general Socket_IO as part of Pure;
2011-09-21 ago wenzelm more hints on Z3 configuration;
2011-09-21 ago wenzelm reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);
2011-09-21 ago nipkow renamed inv -> filter
2011-09-21 ago nipkow Added proofs about narowing
2011-09-21 ago nipkow added missing makefile dependence
2011-09-21 ago nipkow added example
2011-09-21 ago nipkow tuned
2011-09-21 ago nipkow refined comment
2011-09-21 ago kleing fixed two typos in IMP (by Jean Pichon)