src/HOL/Library/reflection.ML
Fri, 02 Mar 2012 15:17:54 +0100 haftmann dropped dead code
Thu, 16 Feb 2012 23:07:01 +0100 wenzelm more antiquotations;
Tue, 08 Nov 2011 11:44:37 +0100 wenzelm tuned;
Mon, 25 Jul 2011 11:21:45 +0200 bulwahn replacing conversion function of old code generator by the current code generator in the reflection tactic
Mon, 25 Jul 2011 11:21:44 +0200 bulwahn fixed typo
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Wed, 20 Apr 2011 14:33:33 +0200 wenzelm explicit context for Codegen.eval_term etc.;
Sat, 16 Apr 2011 20:49:48 +0200 wenzelm proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
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;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Tue, 25 May 2010 20:28:16 +0200 wenzelm eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
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 =)
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Sat, 17 Oct 2009 22:34:19 +0200 wenzelm tuned/moved divide_and_conquer';
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Fri, 10 Jul 2009 07:59:27 +0200 haftmann dropped find_index_eq
Mon, 08 Jun 2009 18:37:35 +0200 hoelzl Added new evaluator "approximate"
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
Wed, 03 Jun 2009 15:48:54 +0200 hoelzl Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
Wed, 03 Jun 2009 11:33:16 +0200 hoelzl Removed usage of reference in reification
Tue, 02 Jun 2009 18:38:13 +0200 hoelzl corrected spacing in reflection
Fri, 24 Apr 2009 08:24:52 +0200 haftmann added helpless comment
Fri, 27 Mar 2009 12:22:02 +0100 haftmann dropped infix union
Fri, 27 Feb 2009 18:03:47 +0100 wenzelm eliminated private clones of List.partition;
Mon, 09 Feb 2009 11:19:44 +0100 hoelzl Proof method 'reify' is now reentrant.
Thu, 05 Feb 2009 11:49:15 +0100 hoelzl Add approximation method
Wed, 28 Jan 2009 11:04:10 +0100 haftmann Reflection.thy now in HOL/Library
less more (0) tip