| 2005-05-31 |
obua |
2005-05-31 |
Removed final_consts from theory data. Now const_deps deals with final
constants.
|
file | diff | annotate |
| 2005-05-31 |
wenzelm |
2005-05-31 |
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
tuned;
|
file | diff | annotate |
| 2005-05-30 |
obua |
2005-05-30 |
Infinite chains in definitions are now detected, too.
|
file | diff | annotate |
| 2005-05-29 |
obua |
2005-05-29 |
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
|
file | diff | annotate |
| 2005-04-16 |
wenzelm |
2005-04-16 |
added del_modesyntax(_i);
|
file | diff | annotate |
| 2005-04-13 |
wenzelm |
2005-04-13 |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Sign.prep_ext_merge;
|
file | diff | annotate |
| 2005-04-13 |
wenzelm |
2005-04-13 |
*** empty log message ***
|
file | diff | annotate |
| 2005-03-03 |
skalberg |
2005-03-03 |
Move towards standard functions.
|
file | diff | annotate |
| 2005-02-13 |
skalberg |
2005-02-13 |
Deleted Library.option type.
|
file | diff | annotate |
| 2004-06-21 |
kleing |
2004-06-21 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| 2004-06-09 |
wenzelm |
2004-06-09 |
Sign.is_logtype;
|
file | diff | annotate |
| 2004-05-29 |
wenzelm |
2004-05-29 |
improved output; refer to Pretty.pp;
|
file | diff | annotate |
| 2004-05-21 |
wenzelm |
2004-05-21 |
Type.strip_sorts;
|
file | diff | annotate |
| 2004-04-22 |
wenzelm |
2004-04-22 |
support for advanced translation functions;
|
file | diff | annotate |
| 2003-10-09 |
skalberg |
2003-10-09 |
Added support for making constants final, that is, ensuring that no
definition can be given later (useful for constants whose behaviour is
fixed axiomatically rather than definitionally).
|
file | diff | annotate |
| 2003-09-23 |
skalberg |
2003-09-23 |
Fixed soundness bug.
|
file | diff | annotate |
| 2003-09-04 |
berghofe |
2003-09-04 |
Changed no_vars such that it outputs list of illegal schematic variables.
|
file | diff | annotate |
| 2002-10-14 |
nipkow |
2002-10-14 |
Ported find_intro/elim to Isar.
|
file | diff | annotate |
| 2002-01-16 |
wenzelm |
2002-01-16 |
GPLed;
|
file | diff | annotate |
| 2001-12-21 |
wenzelm |
2001-12-21 |
hide: flag for full/base name;
|
file | diff | annotate |
| 2001-11-28 |
wenzelm |
2001-11-28 |
theory data: removed obsolete finish method;
|
file | diff | annotate |
| 2001-11-09 |
wenzelm |
2001-11-09 |
theory data: finish method;
|
file | diff | annotate |
| 2001-08-15 |
wenzelm |
2001-08-15 |
support for absolute namespace entry paths;
|
file | diff | annotate |
| 2001-01-18 |
wenzelm |
2001-01-18 |
Sign.exists_stamp;
|
file | diff | annotate |
| 2000-11-18 |
wenzelm |
2000-11-18 |
improved messages;
|
file | diff | annotate |
| 2000-11-06 |
wenzelm |
2000-11-06 |
Sign.typ_instance;
|
file | diff | annotate |
| 2000-08-17 |
wenzelm |
2000-08-17 |
tuned error handling;
|
file | diff | annotate |
| 2000-08-04 |
wenzelm |
2000-08-04 |
axioms: Term.no_dummy_patterns;
|
file | diff | annotate |
| 2000-07-13 |
wenzelm |
2000-07-13 |
tuned cycle_msg;
|
file | diff | annotate |
| 2000-07-13 |
wenzelm |
2000-07-13 |
const_deps: unit Graph.T;
proper merge of const_deps;
tuned;
|
file | diff | annotate |
| 2000-07-08 |
nipkow |
2000-07-08 |
Defs are now checked for circularity (if not overloaded).
|
file | diff | annotate |
| 2000-07-07 |
nipkow |
2000-07-07 |
Tightened up check of types in constant defs.
|
file | diff | annotate |
| 2000-05-21 |
wenzelm |
2000-05-21 |
adapted to inner syntax of sorts;
|
file | diff | annotate |
| 2000-04-17 |
wenzelm |
2000-04-17 |
name space hide operations;
|
file | diff | annotate |
| 1999-07-12 |
wenzelm |
1999-07-12 |
removed merge_theories;
|
file | diff | annotate |
| 1999-05-17 |
wenzelm |
1999-05-17 |
prep_ext exported (again);
|
file | diff | annotate |
| 1999-05-04 |
wenzelm |
1999-05-04 |
hide prep_ext, merge_theories;
|
file | diff | annotate |
| 1999-04-30 |
wenzelm |
1999-04-30 |
theory data: copy;
|
file | diff | annotate |
| 1999-03-17 |
wenzelm |
1999-03-17 |
added assert_super;
|
file | diff | annotate |
| 1999-03-09 |
wenzelm |
1999-03-09 |
token translation: real;
|
file | diff | annotate |
| 1999-02-03 |
wenzelm |
1999-02-03 |
added is_draft;
renamed sig to PRIVATE_THEORY;
|
file | diff | annotate |
| 1998-11-17 |
wenzelm |
1998-11-17 |
Theory.apply replaced by Library.apply;
|
file | diff | annotate |
| 1998-11-14 |
wenzelm |
1998-11-14 |
val copy: theory -> theory;
|
file | diff | annotate |
| 1998-11-09 |
wenzelm |
1998-11-09 |
removed local_theory;
|
file | diff | annotate |
| 1998-10-13 |
wenzelm |
1998-10-13 |
PRIVATE sig parts;
|
file | diff | annotate |
| 1998-06-20 |
wenzelm |
1998-06-20 |
added read_def_axm;
|
file | diff | annotate |
| 1998-06-10 |
wenzelm |
1998-06-10 |
tuned comments;
|
file | diff | annotate |
| 1998-06-05 |
wenzelm |
1998-06-05 |
use Object.T and Object.kind;
added print_data;
improved get_data, put_data: more abstract;
add_axioms(_i), add_oracle: made atomic transactions;
|
file | diff | annotate |
| 1998-05-28 |
wenzelm |
1998-05-28 |
fixed error msgs;
|
file | diff | annotate |
| 1998-05-27 |
paulson |
1998-05-27 |
Changed require to requires for MLWorks
|
file | diff | annotate |
| 1998-05-12 |
wenzelm |
1998-05-12 |
fixed comment;
|
file | diff | annotate |
| 1998-04-29 |
wenzelm |
1998-04-29 |
renamed setup to apply;
added add_nonterminals: bstring list -> theory -> theory;
added parent_path: theory -> theory;
added root_path: theory -> theory;
added require: theory -> string -> string -> unit (from section_utils.ML);
|
file | diff | annotate |
| 1998-04-04 |
wenzelm |
1998-04-04 |
added local_theory (for Isar);
added setup;
|
file | diff | annotate |
| 1998-02-12 |
wenzelm |
1998-02-12 |
Sign.merge vs. Sign.nontriv_merge;
|
file | diff | annotate |
| 1998-02-12 |
wenzelm |
1998-02-12 |
tuned add_trrules;
|
file | diff | annotate |
| 1997-12-28 |
wenzelm |
1997-12-28 |
renamed Symtab.null to Symtab.empty;
renamed Symtan.extend_new to Symtab.extend;
|
file | diff | annotate |
| 1997-12-02 |
wenzelm |
1997-12-02 |
tuned trfuns types;
|
file | diff | annotate |
| 1997-11-20 |
wenzelm |
1997-11-20 |
init_data: improved print method;
|
file | diff | annotate |
| 1997-11-20 |
wenzelm |
1997-11-20 |
tuned infer_types interface;
|
file | diff | annotate |
| 1997-11-05 |
wenzelm |
1997-11-05 |
adapted add_trfunsT;
defs: admit TYPE arguments;
|
file | diff | annotate |