NEWS
Fri, 29 Oct 2010 11:07:21 +0200 wenzelm merged
Fri, 29 Oct 2010 08:44:46 +0200 bulwahn NEWS
Thu, 28 Oct 2010 23:19:52 +0200 wenzelm discontinued obsolete ML antiquotation @{theory_ref};
Tue, 26 Oct 2010 15:06:36 +0200 krauss fixed typo
Tue, 26 Oct 2010 13:50:18 +0200 krauss NEWS
Tue, 26 Oct 2010 11:45:12 +0200 boehmes joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
Mon, 25 Oct 2010 16:18:00 +0200 wenzelm merged
Mon, 25 Oct 2010 16:17:16 +0200 wenzelm significantly improved Isabelle/Isar implementation manual;
Mon, 25 Oct 2010 11:42:05 +0200 blanchet merged
Mon, 25 Oct 2010 10:30:46 +0200 blanchet introduced manual version of "Auto Solve" as "solve_direct"
Mon, 25 Oct 2010 11:16:23 +0200 wenzelm added ML antiquotation @{assert};
Sun, 24 Oct 2010 20:37:30 +0200 nipkow renamed nat_number
Fri, 22 Oct 2010 11:11:34 +0200 blanchet make Sledgehammer minimizer fully work with SMT
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
Thu, 14 Oct 2010 12:40:14 +0200 krauss NEWS
Wed, 06 Oct 2010 17:44:21 +0200 blanchet merged
Tue, 05 Oct 2010 12:06:08 +0200 blanchet document latest changes to Meson/Metis/Sledgehammer
Mon, 04 Oct 2010 14:46:48 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Tue, 28 Sep 2010 15:33:56 +0200 haftmann NEWS
Tue, 28 Sep 2010 09:54:07 +0200 krauss no longer declare .psimps rules as [simp].
Fri, 24 Sep 2010 16:17:59 +0200 wenzelm clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
Thu, 23 Sep 2010 09:53:52 +0200 haftmann CONTRIBUTORS and NEWS
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
Mon, 13 Sep 2010 14:55:21 +0200 haftmann merged
Mon, 13 Sep 2010 14:53:56 +0200 haftmann 'class' and 'type' are now antiquoations by default
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Mon, 13 Sep 2010 08:43:48 +0200 nipkow added and renamed lemmas
Fri, 10 Sep 2010 15:17:44 +0200 wenzelm merged
Thu, 09 Sep 2010 14:38:14 +0200 bulwahn changing String.literal to a type instead of a datatype
Thu, 09 Sep 2010 18:32:21 +0200 wenzelm NEWS: some notes on interrupts;
Wed, 08 Sep 2010 13:25:22 +0200 haftmann NEWS
Tue, 07 Sep 2010 12:04:18 +0200 nipkow renamed expand_*_eq in HOLCF as well
Mon, 06 Sep 2010 22:08:49 +0200 wenzelm ML_Context.thm and ML_Context.thms no longer pervasive;
Mon, 06 Sep 2010 12:38:45 +0200 wenzelm merged;
Sun, 05 Sep 2010 21:39:24 +0200 krauss removed duplicate lemma
Sun, 05 Sep 2010 23:16:21 +0200 wenzelm turned show_brackets into proper configuration option;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Fri, 03 Sep 2010 23:54:48 +0200 wenzelm turned eta_contract into proper configuration option;
Fri, 03 Sep 2010 22:36:16 +0200 wenzelm configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
Fri, 03 Sep 2010 21:13:53 +0200 wenzelm pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
Fri, 03 Sep 2010 12:01:47 +0200 wenzelm merged
Thu, 02 Sep 2010 18:45:23 +0200 hoelzl merged
Thu, 02 Sep 2010 13:32:17 +0200 hoelzl NEWS
Fri, 03 Sep 2010 11:21:58 +0200 wenzelm turned show_consts into proper configuration option;
Thu, 02 Sep 2010 00:48:07 +0200 wenzelm turned show_question_marks into proper configuration option;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Sat, 28 Aug 2010 11:42:33 +0200 haftmann merged
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Fri, 27 Aug 2010 18:00:45 +0200 wenzelm merged
Fri, 27 Aug 2010 14:25:29 +0200 haftmann merged
Fri, 27 Aug 2010 14:25:07 +0200 haftmann official support for Scala
Fri, 27 Aug 2010 14:14:08 +0200 wenzelm structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
Fri, 27 Aug 2010 12:57:55 +0200 wenzelm merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 21:03:14 +0200 haftmann NEWS
Fri, 27 Aug 2010 12:40:20 +0200 wenzelm proper context for various Thy_Output options, via official configuration options in ML and Isar;
Wed, 25 Aug 2010 14:18:09 +0200 wenzelm discontinued obsolete 'global' and 'local' commands;
less more (0) -1000 -300 -100 -60 tip