| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:29:23 +0100 |
haftmann |
constdefs is legacy
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 20:44:42 +0100 |
wenzelm |
declare Spec_Rules for most basic definitional packages;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
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, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
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
|
| Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
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
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:07 +0100 |
wenzelm |
discontinued legacy vars;
|
file |
diff |
annotate
|
| Wed, 07 Nov 2007 16:42:59 +0100 |
wenzelm |
discontinued ProofContext.read_prop_legacy;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 17:58:27 +0200 |
haftmann |
defs are added to code data
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:52 +0200 |
wenzelm |
read prop as prop, not term;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:13 +0200 |
wenzelm |
Thm.def_name_optional;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:48 +0100 |
wenzelm |
LocalDefs.cert_def;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 18:19:28 +0100 |
wenzelm |
tuned LocalTheory.pretty_consts;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:37 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:27 +0100 |
wenzelm |
LocalTheory.pretty_consts;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:06 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:37 +0100 |
wenzelm |
Specification.pretty_consts ctxt;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 23:27:55 +0100 |
wenzelm |
Specification.pretty_consts;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:36 +0200 |
wenzelm |
replaced sign by thy;
|
file |
diff |
annotate
|
| Tue, 17 May 2005 18:10:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:45:25 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 29 Jun 2004 11:18:34 +0200 |
kleing |
license change to BSD
|
file |
diff |
annotate
|
| Fri, 07 May 2004 20:33:37 +0200 |
wenzelm |
be liberal about constant names;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 20:50:51 +0200 |
wenzelm |
improved messages;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 13:26:47 +0200 |
wenzelm |
'constdefs' with automatic type-inference and structure context;
|
file |
diff |
annotate
|