2014-07-21 wenzelm 2014-07-21 refer to Simplifier Trace panel on first invocation;
2014-07-21 wenzelm 2014-07-21 removed unused markup (cf. 2f7d91242b99);
2014-07-21 wenzelm 2014-07-21 regular message to refer to Simplifier Trace panel (unused);
2014-07-21 wenzelm 2014-07-21 proper Swing buttons instead of active areas within text (by Lars Hupel);
2014-07-21 wenzelm 2014-07-21 misc tuning and simplification;
2014-07-21 wenzelm 2014-07-21 clarified "simp_trace_new" and corresponding isar-ref section;
2014-07-21 wenzelm 2014-07-21 more on "Simplifier trace" (by Lars Hupel);
2014-07-21 wenzelm 2014-07-21 always complete explicit symbols;
2014-07-21 wenzelm 2014-07-21 discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-07-21 wenzelm 2014-07-21 updated to jdk-7u65;
2014-07-21 traytel 2014-07-21 regression test for datatypes defined in IsaFoR
2014-07-21 kleing 2014-07-21 ghc mac installation repaired; test back on.
2014-07-20 wenzelm 2014-07-20 proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-20 wenzelm 2014-07-20 updated to jdk-8u11 (inactive);
2014-07-20 wenzelm 2014-07-20 avoid delay_load overrun;
2014-07-20 wenzelm 2014-07-20 provide explicit options file -- avoid multiple Scala/JVM invocation;
2014-07-20 wenzelm 2014-07-20 check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
2014-07-19 kleing 2014-07-19 attempt to run without ISABELLE_GHC setting again on mac-poly
2014-07-19 kleing 2014-07-19 apparently, setting ISABELLE_GHC makes ghc unusable
2014-07-19 haftmann 2014-07-19 reverse induction over nonempty lists
2014-07-19 haftmann 2014-07-19 more appropriate postprocessing of rational numbers: extract sign to front of fraction
2014-07-19 blanchet 2014-07-19 doc fixes (contributed by Christian Sternagel)
2014-07-19 blanchet 2014-07-19 made SML/NJ happier
2014-07-18 kleing 2014-07-18 avoid duplicate fact name
2014-07-18 kleing 2014-07-18 afp-poly runs on macbroy2 (different ghc)
2014-07-18 nipkow 2014-07-18 reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-18 nipkow 2014-07-18 tuned
2014-07-17 hoelzl 2014-07-17 register tree with datatype_compat ot support QuickCheck
2014-07-17 desharna 2014-07-17 fix bug caused by bad context
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-07-16 blanchet 2014-07-16 disabled MaSh for the Isabelle2014 release, due to a couple of issues
2014-07-16 desharna 2014-07-16 refactor commonly used functions
2014-07-16 desharna 2014-07-16 document property 'rel_sel'
2014-07-16 desharna 2014-07-16 generate 'rel_sel' theorem for (co)datatypes
2014-07-16 desharna 2014-07-16 fix rel_cases
2014-07-15 blanchet 2014-07-15 made SML/NJ happier
2014-07-15 kleing 2014-07-15 add ISABELLE_GHC settings for isatest
2014-07-14 noschinl 2014-07-14 mira.py: building jEdit plugin is required for makeall
2014-07-15 blanchet 2014-07-15 took out 'rel_cases' for now because of failing tactic
2014-07-15 blanchet 2014-07-15 record MaSh algorithm in spying data
2014-07-15 blanchet 2014-07-15 tuned whitespace (also in strings)
2014-07-15 blanchet 2014-07-15 also learn when 'fact_filter =' is set explicitly
2014-07-15 blanchet 2014-07-15 no warning in case MaSh is disabled
2014-07-15 blanchet 2014-07-15 don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
2014-07-15 blanchet 2014-07-15 no need for 'mash' subdirectory after removal of Python program
2014-07-14 panny 2014-07-14 fix typo
2014-07-14 panny 2014-07-14 throw error for bad input
2014-07-14 panny 2014-07-14 catch "not found" case
2014-07-12 blanchet 2014-07-12 merge
2014-07-12 blanchet 2014-07-12 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
2014-07-12 blanchet 2014-07-12 tuning
2014-07-12 blanchet 2014-07-12 made SML/NJ happier
2014-07-11 Andreas Lochbihler 2014-07-11 reactivate session Quickcheck_Examples
2014-07-11 Andreas Lochbihler 2014-07-11 adapt and reactivate Quickcheck_Types and add two test cases
2014-07-11 blanchet 2014-07-11 more docs
2014-07-10 blanchet 2014-07-10 lambda-lifting for Z3 Isar proofs
2014-07-10 blanchet 2014-07-10 append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
2014-07-10 blanchet 2014-07-10 avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)
2014-07-09 nipkow 2014-07-09 merged
2014-07-09 nipkow 2014-07-09 added lemmas