| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2009 14:58:15 +0100 |
blanchet |
Added nitpick_const_simp attribute to recdef and record packages.
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 20:27:37 +0200 |
wenzelm |
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Sat, 24 May 2008 22:04:52 +0200 |
wenzelm |
more uniform treatment of OuterSyntax.local_theory commands;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 13:03:09 +0100 |
wenzelm |
eliminated quiete_mode ref (not really needed);
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:36 +0200 |
wenzelm |
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:14:17 +0200 |
berghofe |
Adapted to changes in interface of Specification.theorem_i
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:08 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:29 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:30 +0100 |
wenzelm |
simplified Proof.theorem(_i);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 00:15:39 +0100 |
wenzelm |
recdef_tc(_i): local_theory interface via Specification.theorem_i;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 16:49:21 +0200 |
haftmann |
switched merge_alists'' to AList.merge'' whenever appropriate
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:45 +0200 |
wenzelm |
export get_hints;
|
file |
diff |
annotate
|