src/HOL/HOL.thy
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;
Thu, 29 Apr 2010 15:00:41 +0200 haftmann avoid popular infixes
Wed, 28 Apr 2010 12:07:52 +0200 wenzelm renamed command 'defaultsort' to 'default_sort';
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:26:31 -0700 huffman syntax precedence for If and Let
Sun, 25 Apr 2010 23:09:32 +0200 wenzelm renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
Fri, 23 Apr 2010 19:36:04 +0200 wenzelm removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
Wed, 21 Apr 2010 12:10:52 +0200 bulwahn added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Mon, 29 Mar 2010 14:49:53 +0200 blanchet reintroduce efficient set structure to collect "no_atp" theorems
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Wed, 17 Mar 2010 12:01:01 +0100 blanchet fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
Wed, 17 Mar 2010 09:14:43 +0100 blanchet added support for "specification" and "ax_specification" constructs to Nitpick
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 26 Feb 2010 21:43:26 +0100 wenzelm tuned hyp_subst_tac';
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Sun, 31 Jan 2010 15:22:40 +0100 berghofe merged
Sat, 30 Jan 2010 16:59:49 +0100 berghofe Added setup for simplification of equality constraints in cases rules.
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 15 Jan 2010 14:43:00 +0100 berghofe merged
Sun, 10 Jan 2010 18:03:20 +0100 berghofe Added setup for simplification of equality constraints in induction rules.
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Mon, 11 Jan 2010 16:45:02 +0100 haftmann tuned code equations
Fri, 08 Jan 2010 14:34:17 +0100 haftmann boolean operators for scala
less more (0) -300 -100 -60 tip