NEWS
2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 kuncar 2015-05-04 NEWS
2015-05-04 nipkow 2015-05-04 no more simp_legacy_precond
2015-04-19 wenzelm 2015-04-19 back to post-release mode -- after fork point;
2015-04-17 wenzelm 2015-04-17 added Eisbach, using version 3752768caa17 of its Bitbucket repository;
2015-04-17 wenzelm 2015-04-17 tuned;
2015-04-17 wenzelm 2015-04-17 tuned for release;
2015-04-17 traytel 2015-04-17 (low importance) NEWS
2015-04-17 wenzelm 2015-04-17 allow to exclude session groups;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-16 wenzelm 2015-04-16 clarified thy_deps;
2015-04-16 wenzelm 2015-04-16 let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-15 wenzelm 2015-04-15 NEWS;
2015-04-14 wenzelm 2015-04-14 NEWS;
2015-04-12 wenzelm 2015-04-12 tuned;
2015-04-11 paulson 2015-04-11 Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
2015-04-11 wenzelm 2015-04-11 tuned spelling;
2015-04-11 wenzelm 2015-04-11 misc tuning for release;
2015-04-10 wenzelm 2015-04-10 tuned;
2015-04-10 nipkow 2015-04-10 renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
2015-04-09 wenzelm 2015-04-09 merged
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-09 blanchet 2015-04-09 introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
2015-04-08 blanchet 2015-04-08 tuned wording
2015-04-08 blanchet 2015-04-08 Z3 news
2015-04-08 blanchet 2015-04-08 renamed multiset ordering to free up nice <# etc. symbols for the standard subset
2015-04-08 wenzelm 2015-04-08 misc tuning for release;
2015-04-07 nipkow 2015-04-07 Removed mcard because it is equal to size
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-04 wenzelm 2015-04-04 some explanation of 'private';
2015-04-01 wenzelm 2015-04-01 merged
2015-04-01 wenzelm 2015-04-01 added command 'experiment';
2015-04-01 wenzelm 2015-04-01 NEWS;
2015-04-01 wenzelm 2015-04-01 added isabelle build option -x, to exclude sessions;
2015-04-01 wenzelm 2015-04-01 added isabelle build option -k, for fast off-line checking of theory sources;
2015-04-01 paulson 2015-04-01 HOL Light Libraries for complex Arctan, Arcsin, Arccos
2015-03-31 haftmann 2015-03-31 NEWS
2015-03-30 wenzelm 2015-03-30 clarified NEWS (cf. 97872c658a44);
2015-03-29 wenzelm 2015-03-29 rule_insts_schematic is considered legacy and false by default;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-25 blanchet 2015-03-25 more multiset theorems
2015-03-25 wenzelm 2015-03-25 NEWS;
2015-03-24 wenzelm 2015-03-24 admit dummy patterns in instantiations; clarified context;
2015-03-23 wenzelm 2015-03-23 NEWS;
2015-03-19 paulson 2015-03-19 New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-18 paulson 2015-03-18 new HOL Light material about exp, sin, cos
2015-03-18 noschinl 2015-03-18 added proof method rewrite
2015-03-17 paulson 2015-03-17 Merge
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 blanchet 2015-03-10 documented renamed theories
2015-03-09 wenzelm 2015-03-09 merged
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2015-03-09 paulson 2015-03-09 Removed the infix operator "choose" to allow HOLCF to build
2015-03-07 wenzelm 2015-03-07 NEWS;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 nipkow 2015-03-04 merged
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-28 haftmann 2015-02-28 spelling