NEWS
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
less more (0) -1000 -300 -100 -60 tip