| 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
|
| Mon, 24 Jan 2005 17:59:48 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 18:45:56 +0200 |
berghofe |
Replaced quote by Library.quote, since quote now refers to Symbol.quote
|
file |
diff |
annotate
|
| Thu, 03 Jan 2002 17:56:15 +0100 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Thu, 01 Nov 2001 21:12:13 +0100 |
wenzelm |
Goals.add_locale;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2001 21:03:43 +0200 |
wenzelm |
legacy interfaces for axclass instantiation;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 18:52:30 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:20:33 +0200 |
wenzelm |
defs (overloaded);
|
file |
diff |
annotate
|
| Sun, 21 May 2000 14:35:27 +0200 |
wenzelm |
adapted to inner syntax of sorts;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:25:52 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
| Mon, 17 May 1999 21:36:34 +0200 |
wenzelm |
cleaned comments;
|
file |
diff |
annotate
|
| Wed, 12 May 1999 17:26:56 +0200 |
wenzelm |
strip_quotes replaced by unenclose;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 13:42:42 +0100 |
wenzelm |
adapted AxClass.add_axclass;
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 21:52:49 +0100 |
wenzelm |
tuned space;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:18:02 +0100 |
wenzelm |
IsarThy.begin/end_theory;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 17:28:02 +0100 |
wenzelm |
get_lexicon;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:39:41 +0100 |
wenzelm |
eliminated Attribute structure;
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:50:37 +0100 |
paulson |
more efficient strip_quotes using "substring"
|
file |
diff |
annotate
|
| Fri, 11 Dec 1998 10:36:39 +0100 |
paulson |
the + facility for locales, by Florian
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:42:53 +0100 |
paulson |
locales: assumes and defines may be empty
|
file |
diff |
annotate
|
| Tue, 17 Nov 1998 14:07:04 +0100 |
wenzelm |
Theory.apply replaced by Library.apply;
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:26:47 +0200 |
wenzelm |
Syntax.max_pri;
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 18:23:57 +0200 |
wenzelm |
added 'locale' section;
|
file |
diff |
annotate
|
| Sat, 20 Jun 1998 20:18:22 +0200 |
wenzelm |
export mk_triple1/2;
|
file |
diff |
annotate
|
| Mon, 25 May 1998 21:27:22 +0200 |
wenzelm |
tuned local, global;
|
file |
diff |
annotate
|
| Wed, 20 May 1998 18:56:59 +0200 |
wenzelm |
tuned keywords;
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:26:59 +0200 |
wenzelm |
replaced thy_setup by 'setup' section;
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 11:41:24 +0200 |
wenzelm |
replaced thy_data by thy_setup;
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:14:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 29 Dec 1997 14:29:34 +0100 |
wenzelm |
removed distinct_fst_string;
|
file |
diff |
annotate
|
| Thu, 04 Dec 1997 13:49:27 +0100 |
wenzelm |
moved global_names ref to Pure/ROOT.ML;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 21:04:51 +0100 |
wenzelm |
added MLtext section;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 17:55:55 +0100 |
wenzelm |
tuned: distinct_fst_string;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 14:09:16 +0100 |
wenzelm |
export const_decls parser;
|
file |
diff |
annotate
|
| Fri, 31 Oct 1997 15:28:01 +0100 |
wenzelm |
dup sections: warning instead of error;
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 17:00:34 +0100 |
wenzelm |
added thy_data;
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:32:38 +0100 |
wenzelm |
PureThy.add_store_defs, PureThy.add_store_axioms;
|
file |
diff |
annotate
|
| Mon, 27 Oct 1997 15:43:53 +0100 |
wenzelm |
flipped global_names default;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:44:46 +0200 |
wenzelm |
improved typ parser, exported;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 17:08:18 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 10:38:16 +0200 |
wenzelm |
local section;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 11:10:54 +0200 |
paulson |
Eta-expanded a function decl to make sml/nj happy
|
file |
diff |
annotate
|
| Thu, 16 Oct 1997 14:48:10 +0200 |
wenzelm |
removed begin;
|
file |
diff |
annotate
|
| Wed, 15 Oct 1997 15:14:56 +0200 |
wenzelm |
eliminated aliasing merge: now always extends;
|
file |
diff |
annotate
|
| Thu, 09 Oct 1997 14:53:31 +0200 |
wenzelm |
improved oracle: name;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 20:00:31 +0200 |
wenzelm |
fixed 'begin';
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 19:39:40 +0200 |
wenzelm |
optional begin keyword;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 18:29:11 +0200 |
wenzelm |
added 'path' section;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 18:19:44 +0200 |
wenzelm |
fully qualified name: Theory.set_oracle;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 17:40:09 +0200 |
wenzelm |
fully qualified names: Theory.add_XXX;
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:36:03 +0200 |
wenzelm |
renamed |-> <-| <-> to Parse/PrintRule;
|
file |
diff |
annotate
|
| Tue, 06 May 1997 12:55:07 +0200 |
wenzelm |
removed MLtrans, MLtext;
|
file |
diff |
annotate
|
| Fri, 28 Feb 1997 16:40:08 +0100 |
wenzelm |
added token_translation interface;
|
file |
diff |
annotate
|
| Fri, 13 Dec 1996 17:37:42 +0100 |
wenzelm |
added typed print translations;
|
file |
diff |
annotate
|
| Tue, 10 Dec 1996 12:50:35 +0100 |
wenzelm |
syntax section: added 'output' mode option;
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 16:40:23 +0100 |
wenzelm |
use_thy now automatically opens theory structures;
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 16:33:59 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
| Mon, 18 Nov 1996 17:31:14 +0100 |
wenzelm |
mixfix: added syntax for Infirl/rName;
|
file |
diff |
annotate
|
| Thu, 11 Jul 1996 15:18:57 +0200 |
paulson |
Oracles can now be strings instead of identifiers
|
file |
diff |
annotate
|
| Tue, 18 Jun 1996 16:17:38 +0200 |
paulson |
Translation infixes <->, etc., no longer available at top-level
|
file |
diff |
annotate
|
| Tue, 30 Apr 1996 13:40:32 +0200 |
clasohm |
changed ident_no_colon so that it forbids postfix "=", too
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 14:11:41 +0100 |
clasohm |
added constdefs
|
file |
diff |
annotate
|
| Tue, 05 Mar 1996 15:52:59 +0100 |
paulson |
Addition of oracles
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Fri, 01 Dec 1995 13:54:27 +0100 |
clasohm |
added const_type to type_decl
|
file |
diff |
annotate
|
| Fri, 01 Dec 1995 12:22:07 +0100 |
clasohm |
simplified parser for constType
|
file |
diff |
annotate
|
| Wed, 29 Nov 1995 16:47:38 +0100 |
clasohm |
added type class to simple_type
|
file |
diff |
annotate
|
| Tue, 07 Nov 1995 12:57:20 +0100 |
clasohm |
types in consts section of .thy files can now be specified without quotes
|
file |
diff |
annotate
|
| Wed, 06 Sep 1995 15:27:11 +0200 |
clasohm |
removed list2 and enum2
|
file |
diff |
annotate
|
| Wed, 06 Sep 1995 15:11:19 +0200 |
clasohm |
added enum2 and list2
|
file |
diff |
annotate
|
| Mon, 21 Aug 1995 18:03:12 +0200 |
wenzelm |
minor fix to make less noise with SML/NJ;
|
file |
diff |
annotate
|
| Tue, 11 Apr 1995 11:20:43 +0200 |
nipkow |
(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).
|
file |
diff |
annotate
|
| Fri, 27 Jan 1995 13:40:07 +0100 |
wenzelm |
binder: optional body pri now [bracketted];
|
file |
diff |
annotate
|
| Wed, 18 Jan 1995 11:36:04 +0100 |
clasohm |
added optional precedence for body of binder;
|
file |
diff |
annotate
|
| Fri, 09 Dec 1994 16:44:31 +0100 |
wenzelm |
minor internal changes;
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 12:34:47 +0100 |
clasohm |
moved first call of store_theory from thy_read.ML to created .thy.ML file
|
file |
diff |
annotate
|
| Mon, 14 Nov 1994 11:57:32 +0100 |
wenzelm |
exported 'cat';
|
file |
diff |
annotate
|
| Tue, 25 Oct 1994 13:16:49 +0100 |
wenzelm |
strip_quotes now exported;
|
file |
diff |
annotate
|
| Wed, 12 Oct 1994 16:30:19 +0100 |
wenzelm |
type_args, opt_witness now exported;
|
file |
diff |
annotate
|
| Wed, 07 Sep 1994 10:43:30 +0200 |
clasohm |
renamed temporary variable 'base' to 'thy' in mk_structure
|
file |
diff |
annotate
|
| Tue, 06 Sep 1994 14:44:10 +0200 |
clasohm |
renamed base_on into mk_base and moved it to the beginning of the generated
|
file |
diff |
annotate
|
| Mon, 22 Aug 1994 11:07:40 +0200 |
lcp |
Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens,
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 15:38:50 +0200 |
wenzelm |
renamed 'defns' to 'defs';
|
file |
diff |
annotate
|
| Fri, 15 Jul 1994 13:30:42 +0200 |
clasohm |
added check for concistency of filename and theory name;
|
file |
diff |
annotate
|
| Wed, 06 Jul 1994 14:39:32 +0200 |
wenzelm |
exported opt_infix, opt_mixfix parsers;
|
file |
diff |
annotate
|
| Thu, 16 Jun 1994 12:07:40 +0200 |
wenzelm |
added 'subclass' section;
|
file |
diff |
annotate
|
| Wed, 01 Jun 1994 15:49:46 +0200 |
wenzelm |
added signature constraint;
|
file |
diff |
annotate
|
| Thu, 19 May 1994 16:26:19 +0200 |
wenzelm |
(replaces Thy/parse.ML and Thy/syntax.ML)
|
file |
diff |
annotate
|