| Sat, 09 Aug 2008 22:43:46 +0200 |
unified Args.T with OuterLex.token, renamed some operations;
|
file | diff | annotate |
| Mon, 04 Aug 2008 20:27:37 +0200 |
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
|
file | diff | annotate |
| Wed, 25 Jun 2008 17:38:32 +0200 |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file | diff | annotate |
| Sat, 24 May 2008 22:04:52 +0200 |
more uniform treatment of OuterSyntax.local_theory commands;
|
file | diff | annotate |
| Sat, 29 Mar 2008 13:03:09 +0100 |
eliminated quiete_mode ref (not really needed);
|
file | diff | annotate |
| Wed, 19 Mar 2008 22:27:57 +0100 |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file | diff | annotate |
| Tue, 09 Oct 2007 17:10:36 +0200 |
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file | diff | annotate |
| Sat, 06 Oct 2007 16:50:04 +0200 |
simplified interfaces for outer syntax;
|
file | diff | annotate |
| Tue, 25 Sep 2007 17:06:14 +0200 |
proper Sign operations instead of Theory aliases;
|
file | diff | annotate |
| Tue, 18 Sep 2007 07:36:15 +0200 |
distinction between regular and default code theorems
|
file | diff | annotate |
| Tue, 28 Aug 2007 18:14:17 +0200 |
Adapted to changes in interface of Specification.theorem_i
|
file | diff | annotate |
| Sun, 29 Jul 2007 14:29:54 +0200 |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file | diff | annotate |
| Mon, 07 May 2007 00:49:59 +0200 |
simplified DataFun interfaces;
|
file | diff | annotate |
| Mon, 26 Feb 2007 23:18:24 +0100 |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file | diff | annotate |
| Fri, 19 Jan 2007 22:08:08 +0100 |
moved parts of OuterParse to SpecParse;
|
file | diff | annotate |
| Thu, 23 Nov 2006 22:38:29 +0100 |
prefer Proof.context over Context.generic;
|
file | diff | annotate |
| Tue, 21 Nov 2006 18:07:30 +0100 |
simplified Proof.theorem(_i);
|
file | diff | annotate |
| Tue, 14 Nov 2006 00:15:39 +0100 |
recdef_tc(_i): local_theory interface via Specification.theorem_i;
|
file | diff | annotate |
| Mon, 23 Oct 2006 16:49:21 +0200 |
switched merge_alists'' to AList.merge'' whenever appropriate
|
file | diff | annotate |
| Fri, 20 Oct 2006 17:07:26 +0200 |
slight cleanup
|
file | diff | annotate |
| Wed, 02 Aug 2006 22:26:45 +0200 |
export get_hints;
|
file | diff | annotate |
| Mon, 05 Jun 2006 14:26:07 +0200 |
HOL/Tools/function_package: Added support for mutual recursive definitions.
|
file | diff | annotate |
| Sat, 20 May 2006 23:36:55 +0200 |
List.partition;
|
file | diff | annotate |
| Sun, 07 May 2006 00:22:05 +0200 |
removed 'concl is' patterns;
|
file | diff | annotate |
| Fri, 05 May 2006 17:17:21 +0200 |
First usable version of the new function definition package (HOL/function_packake/...).
|
file | diff | annotate |
| Thu, 02 Feb 2006 10:24:06 +0100 |
Exporting recdef's hints for use by new recdef package
|
file | diff | annotate |
| Fri, 27 Jan 2006 19:03:02 +0100 |
moved theorem tags from Drule to PureThy;
|
file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 |
simplified type attribute;
|
file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 |
setup: theory -> theory;
|
file | diff | annotate |
| Sat, 14 Jan 2006 22:25:34 +0100 |
generic attributes;
|
file | diff | annotate |
| Fri, 16 Dec 2005 09:00:11 +0100 |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file | diff | annotate |
| Fri, 09 Dec 2005 09:06:45 +0100 |
oriented result pairs in PureThy
|
file | diff | annotate |
| Wed, 19 Oct 2005 21:52:32 +0200 |
removed obsolete add_recdef_old;
|
file | diff | annotate |
| Fri, 23 Sep 2005 09:00:19 +0200 |
temporarily re-introduced overwrite_warn
|
file | diff | annotate |
| Wed, 21 Sep 2005 17:25:32 +0200 |
introduces update_warn instead of overwrite_warn
|
file | diff | annotate |
| Tue, 20 Sep 2005 08:21:49 +0200 |
slight adaptions to library changes
|
file | diff | annotate |
| Thu, 15 Sep 2005 17:16:56 +0200 |
TableFun/Symtab: curried lookup and update;
|
file | diff | annotate |
| Tue, 13 Sep 2005 22:19:19 +0200 |
tuned IsarThy.theorem_i;
|
file | diff | annotate |
| Mon, 05 Sep 2005 17:38:18 +0200 |
curried_lookup/update;
|
file | diff | annotate |
| Tue, 16 Aug 2005 13:42:26 +0200 |
OuterKeyword;
|
file | diff | annotate |
| Fri, 01 Jul 2005 14:14:40 +0200 |
Adapted to new interface of RecfunCodegen.add.
|
file | diff | annotate |
| Fri, 17 Jun 2005 18:35:27 +0200 |
accomodate change of TheoryDataFun;
|
file | diff | annotate |
| Sat, 11 Jun 2005 22:15:48 +0200 |
refer to name spaces values instead of names;
|
file | diff | annotate |
| Tue, 31 May 2005 11:53:13 +0200 |
renamed cond_extern to extern;
|
file | diff | annotate |
| Wed, 13 Apr 2005 18:45:25 +0200 |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file | diff | annotate |
| Wed, 13 Apr 2005 18:34:22 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 |
Move towards standard functions.
|
file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 |
Deleted Library.option type.
|
file | diff | annotate |
| Mon, 24 Jan 2005 18:07:10 +0100 |
Replaced xstring by thmref.
|
file | diff | annotate |
| Sun, 11 Jul 2004 20:33:22 +0200 |
local_cla/simpset_of;
|
file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| Fri, 17 Oct 2003 11:04:36 +0200 |
Prevent recdef from looping when the inductio rule is simplified
|
file | diff | annotate |
| Tue, 12 Feb 2002 20:28:27 +0100 |
got rid of explicit marginal comments (now stripped earlier from input);
|
file | diff | annotate |
| Tue, 15 Jan 2002 00:08:51 +0100 |
removed case_numbers (already covered by default);
|
file | diff | annotate |
| Fri, 11 Jan 2002 00:28:24 +0100 |
clarified IsarThy.apply_theorems_i;
|
file | diff | annotate |
| Thu, 10 Jan 2002 01:11:43 +0100 |
simplified IsarThy.theorem_i;
|
file | diff | annotate |
| Mon, 10 Dec 2001 15:34:15 +0100 |
Recursive equations to be used for code generation are now registered
|
file | diff | annotate |
| Wed, 05 Dec 2001 03:06:05 +0100 |
tuned;
|
file | diff | annotate |
| Wed, 28 Nov 2001 00:46:26 +0100 |
theory data: removed obsolete finish method;
|
file | diff | annotate |