NEWS
Mon, 08 Nov 2010 12:13:44 +0100 boehmes better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
Sat, 06 Nov 2010 00:10:32 +0100 krauss abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
Fri, 05 Nov 2010 23:19:20 +0100 wenzelm moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
Thu, 04 Nov 2010 09:54:16 +0100 haftmann merged
Wed, 03 Nov 2010 12:20:33 +0100 haftmann Theory Multiset provides stable quicksort implementation of sort_key.
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR;
Sun, 31 Oct 2010 11:45:45 +0100 nipkow merged
Fri, 29 Oct 2010 17:57:36 +0200 nipkow Plus -> Sum_Type.Plus
Sat, 30 Oct 2010 21:08:20 +0200 wenzelm support for real valued preferences;
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options;
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;
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Fri, 20 Aug 2010 17:48:30 +0200 haftmann split and enriched theory SetsAndFunctions
Thu, 19 Aug 2010 17:41:52 +0200 wenzelm merged
Thu, 19 Aug 2010 16:08:53 +0200 haftmann deglobalized named HOL constants
Wed, 18 Aug 2010 17:03:09 +0200 haftmann merged
Wed, 18 Aug 2010 17:01:12 +0200 haftmann NEWS
Wed, 18 Aug 2010 15:01:57 +0200 haftmann more helpful NEWS entry
Tue, 17 Aug 2010 16:44:21 +0200 haftmann preemptive NEWS
Wed, 18 Aug 2010 14:55:09 +0200 haftmann NEWS
Wed, 18 Aug 2010 12:26:48 +0200 haftmann deglobalization
Tue, 17 Aug 2010 18:41:55 +0200 wenzelm discontinued support for Poly/ML 5.0 and 5.1 versions;
Tue, 17 Aug 2010 14:33:39 +0200 haftmann NEWS and CONTRIBUTORS
Wed, 11 Aug 2010 14:31:40 +0200 haftmann NEWS
Tue, 03 Aug 2010 16:33:11 +0200 wenzelm theory loading: only the master source file is looked-up in the implicit load path;
Sat, 31 Jul 2010 23:32:05 +0200 ballarin Documentation of 'interpret' updated.
Thu, 22 Jul 2010 22:31:20 +0200 wenzelm discontinued special treatment of ML files -- no longer complete extensions on demand;
Wed, 21 Jul 2010 15:02:51 +0200 wenzelm ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
Wed, 14 Jul 2010 14:53:44 +0200 haftmann export_code without file prints to standard output
Wed, 07 Jul 2010 08:25:22 +0200 bulwahn added NEWS entry
Fri, 02 Jul 2010 10:47:50 +0200 haftmann fixed spelling
Thu, 01 Jul 2010 16:55:05 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
Thu, 01 Jul 2010 10:57:19 +0200 hoelzl Updated NEWS
Tue, 29 Jun 2010 07:55:18 +0200 haftmann merged
Mon, 28 Jun 2010 15:32:06 +0200 haftmann dropped ancient infix mem; refined code generation operations in List.thy
Mon, 28 Jun 2010 15:03:07 +0200 haftmann merged constants "split" and "prod_case"
Fri, 25 Jun 2010 11:48:37 +0200 wenzelm explicit treatment of UTF8 sequences as Isabelle symbols;
Mon, 21 Jun 2010 17:41:57 +0200 wenzelm merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
Tue, 15 Jun 2010 07:42:48 +0200 haftmann merged
Mon, 14 Jun 2010 12:01:30 +0200 haftmann NEWS
Mon, 14 Jun 2010 15:10:36 +0200 haftmann removed simplifier congruence rule of "prod_case"
Thu, 10 Jun 2010 12:24:01 +0200 haftmann qualified type "*"; qualified constants Pair, fst, snd, split
Tue, 08 Jun 2010 16:37:19 +0200 haftmann qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
Mon, 07 Jun 2010 17:39:32 +0200 wenzelm back to non-release mode;
Mon, 21 Jun 2010 11:24:19 +0200 wenzelm final tuning; Isabelle2009-2
Fri, 11 Jun 2010 13:25:28 +0200 wenzelm NEWS: IsabelleText font;
Mon, 07 Jun 2010 17:52:30 +0200 berghofe Documented changes in induct, cases, and nominal_induct method.
Mon, 07 Jun 2010 11:42:32 +0200 wenzelm more NEWS;
Mon, 07 Jun 2010 11:27:08 +0200 wenzelm more NEWS;
Fri, 04 Jun 2010 16:02:46 +0200 krauss NEWS (more strict internal axioms/defs format)
Fri, 04 Jun 2010 11:30:46 +0200 wenzelm spelling;
Thu, 03 Jun 2010 22:17:36 +0200 wenzelm diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
Thu, 03 Jun 2010 16:39:50 +0200 krauss clarified
Thu, 03 Jun 2010 16:39:05 +0200 krauss mention unconstrain in NEWS
Wed, 02 Jun 2010 21:53:03 +0200 wenzelm improved parallelism of proof term normalization;
Tue, 01 Jun 2010 17:52:19 +0200 blanchet merged
Tue, 01 Jun 2010 17:52:00 +0200 blanchet update NEWS
Tue, 01 Jun 2010 15:38:47 +0200 blanchet removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
less more (0) -1000 -120 tip