| Tue, 08 Nov 2011 11:44:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 11:21:44 +0200 |
bulwahn |
fixed typo
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 14:33:33 +0200 |
wenzelm |
explicit context for Codegen.eval_term etc.;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Tue, 25 May 2010 20:28:16 +0200 |
wenzelm |
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| 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 =)
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 22:34:19 +0200 |
wenzelm |
tuned/moved divide_and_conquer';
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:27 +0200 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 18:37:35 +0200 |
hoelzl |
Added new evaluator "approximate"
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 15:48:54 +0200 |
hoelzl |
Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 11:33:16 +0200 |
hoelzl |
Removed usage of reference in reification
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 18:38:13 +0200 |
hoelzl |
corrected spacing in reflection
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 08:24:52 +0200 |
haftmann |
added helpless comment
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 12:22:02 +0100 |
haftmann |
dropped infix union
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 18:03:47 +0100 |
wenzelm |
eliminated private clones of List.partition;
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 11:19:44 +0100 |
hoelzl |
Proof method 'reify' is now reentrant.
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 11:49:15 +0100 |
hoelzl |
Add approximation method
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
| base
|