src/HOL/HOL.thy
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 03 Dec 2010 17:59:13 +0100 wenzelm setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
Wed, 01 Dec 2010 18:00:40 +0100 haftmann merged
Wed, 01 Dec 2010 11:33:17 +0100 haftmann file for package tool type_mapper carries the same name as its Isar command
Wed, 01 Dec 2010 14:56:07 +0100 wenzelm simplified HOL.eq simproc matching;
Fri, 26 Nov 2010 17:54:15 +0100 wenzelm lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
Wed, 17 Nov 2010 11:09:18 +0100 haftmann module for functorial mappers
Wed, 27 Oct 2010 19:14:33 +0200 blanchet reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
Wed, 29 Sep 2010 11:02:24 +0200 krauss backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
Mon, 27 Sep 2010 12:01:04 +0200 blanchet merged
Mon, 27 Sep 2010 09:17:24 +0200 blanchet comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
Mon, 27 Sep 2010 11:11:59 +0200 haftmann corrected OCaml operator precedence
Mon, 20 Sep 2010 18:43:18 +0200 haftmann Pure equality is a regular cpde operation
Thu, 16 Sep 2010 16:51:33 +0200 haftmann adjusted to changes in Code_Runtime
Wed, 15 Sep 2010 20:47:14 +0200 wenzelm dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
Wed, 15 Sep 2010 16:47:31 +0200 haftmann introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
Wed, 15 Sep 2010 15:40:35 +0200 haftmann Code_Runtime.value, corresponding to ML_Context.value
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime
Wed, 15 Sep 2010 11:30:32 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
Sat, 11 Sep 2010 16:36:23 +0200 blanchet added Auto Try to the mix of automatic tools
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Thu, 02 Sep 2010 13:45:39 +0200 blanchet merged
Thu, 02 Sep 2010 11:29:02 +0200 blanchet use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
Thu, 02 Sep 2010 11:42:50 +0200 haftmann merged
Thu, 02 Sep 2010 10:29:47 +0200 haftmann avoid cyclic modules
Thu, 02 Sep 2010 09:13:28 +0200 haftmann merged
Thu, 02 Sep 2010 09:13:16 +0200 haftmann normalization is allowed to solve True
Thu, 02 Sep 2010 08:51:16 +0200 blanchet merged
Thu, 02 Sep 2010 08:29:30 +0200 blanchet merged
Wed, 01 Sep 2010 00:03:15 +0200 blanchet finish moving file
Thu, 02 Sep 2010 08:40:25 +0200 haftmann normalization fails on unchanged goal
Wed, 01 Sep 2010 15:01:12 +0200 haftmann tuned text segment
Tue, 31 Aug 2010 21:01:47 +0200 blanchet fiddling with "try"
Mon, 30 Aug 2010 09:37:43 +0200 haftmann hide all-too-popular constant name eq
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
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 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Thu, 26 Aug 2010 12:19:49 +0200 haftmann prevent line breaks after Scala symbolic operators
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Wed, 25 Aug 2010 14:18:09 +0200 wenzelm discontinued obsolete 'global' and 'local' commands;
Mon, 23 Aug 2010 11:09:49 +0200 haftmann refined and unified naming convention for dynamic code evaluation techniques
Thu, 19 Aug 2010 16:03:07 +0200 haftmann deglobalized named HOL constants
Thu, 19 Aug 2010 10:27:02 +0200 haftmann tuned declaration order
Wed, 18 Aug 2010 14:55:09 +0200 haftmann qualified constants Let and If
Mon, 19 Jul 2010 11:55:42 +0200 haftmann optional break
Mon, 12 Jul 2010 21:38:37 +0200 wenzelm moved misc legacy stuff from OldGoals to Misc_Legacy;
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
Mon, 14 Jun 2010 10:38:29 +0200 haftmann dropped unused bindings
Tue, 01 Jun 2010 15:38:47 +0200 blanchet removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Sun, 09 May 2010 19:15:21 +0200 wenzelm just one version of Thm.unconstrainT, which affects all variables;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Tue, 04 May 2010 14:10:42 +0200 berghofe merged
Tue, 04 May 2010 12:26:46 +0200 berghofe induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
less more (0) -300 -100 -60 tip