src/HOL/HOL.thy
Thu, 05 Jul 2012 16:58:03 +0200 wenzelm removed obsolete rev_contrapos (cf. 1d195de59497);
Tue, 05 Jun 2012 07:10:51 +0200 haftmann prefer sys.error over plain error in Scala to avoid deprecation warning
Thu, 19 Apr 2012 19:36:24 +0200 haftmann moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
Fri, 16 Mar 2012 22:31:19 +0100 wenzelm modernized axiomatization;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 11 Jan 2012 21:04:22 +0100 wenzelm more conventional eval_tac vs. method_setup "eval";
Mon, 09 Jan 2012 18:29:42 +0100 wenzelm prefer antiquotations;
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Wed, 19 Oct 2011 08:37:16 +0200 bulwahn removing old code generator setup in the HOL theory
Wed, 12 Oct 2011 22:48:23 +0200 wenzelm modernized structure Induct_Tacs;
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Thu, 18 Aug 2011 13:25:17 +0200 haftmann moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Wed, 03 Aug 2011 13:59:59 +0200 bulwahn removing the SML evaluator
Sat, 02 Jul 2011 22:55:58 +0200 haftmann install case certificate for If after code_datatype declaration for bool
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sat, 14 May 2011 13:32:33 +0200 wenzelm simplified BLAST_DATA;
Sat, 14 May 2011 11:42:43 +0200 wenzelm modernized functor names;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Tue, 26 Apr 2011 21:27:01 +0200 wenzelm simplified Blast setup;
Fri, 22 Apr 2011 15:05:04 +0200 wenzelm misc tuning and simplification;
Fri, 22 Apr 2011 14:30:32 +0200 wenzelm proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
Fri, 22 Apr 2011 13:58:13 +0200 wenzelm modernized Quantifier1 simproc setup;
Fri, 22 Apr 2011 12:46:48 +0200 wenzelm clarified simpset setup;
Wed, 20 Apr 2011 14:33:33 +0200 wenzelm explicit context for Codegen.eval_term etc.;
Wed, 20 Apr 2011 11:21:12 +0200 wenzelm merged
Wed, 20 Apr 2011 07:44:23 +0200 bulwahn making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
Tue, 19 Apr 2011 23:57:28 +0200 wenzelm eliminated Codegen.mode in favour of explicit argument;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Thu, 31 Mar 2011 09:43:36 +0200 haftmann corrected infix precedence for boolean operators in Haskell
Tue, 22 Mar 2011 20:44:47 +0100 wenzelm more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
Mon, 28 Feb 2011 15:06:36 +0000 paulson declare ext [intro]: Extensionality now available by default
Wed, 23 Feb 2011 11:23:26 +0100 noschinl setup case_product attribute in HOL and FOL
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Thu, 27 Jan 2011 16:24:29 +0100 wenzelm CRITICAL markup for critical poking with unsynchronized references;
Fri, 17 Dec 2010 18:33:35 +0100 wenzelm merged
Fri, 17 Dec 2010 18:24:44 +0100 haftmann avoid slightly odd Conv.tap_thy
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Wed, 15 Dec 2010 09:47:12 +0100 haftmann simplified evaluation function names
Tue, 07 Dec 2010 09:58:56 +0100 blanchet load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
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
less more (0) -300 -100 -60 tip