src/Pure/theory.ML
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i);
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Sign.prep_ext_merge;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-09 wenzelm 2004-06-09 Sign.is_logtype;
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 Type.strip_sorts;
2004-04-22 wenzelm 2004-04-22 support for advanced translation functions;
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).
2003-09-23 skalberg 2003-09-23 Fixed soundness bug.
2003-09-04 berghofe 2003-09-04 Changed no_vars such that it outputs list of illegal schematic variables.
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-21 wenzelm 2001-12-21 hide: flag for full/base name;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-08-15 wenzelm 2001-08-15 support for absolute namespace entry paths;
2001-01-18 wenzelm 2001-01-18 Sign.exists_stamp;
2000-11-18 wenzelm 2000-11-18 improved messages;
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-08-17 wenzelm 2000-08-17 tuned error handling;
2000-08-04 wenzelm 2000-08-04 axioms: Term.no_dummy_patterns;
2000-07-13 wenzelm 2000-07-13 tuned cycle_msg;
2000-07-13 wenzelm 2000-07-13 const_deps: unit Graph.T; proper merge of const_deps; tuned;
2000-07-08 nipkow 2000-07-08 Defs are now checked for circularity (if not overloaded).
2000-07-07 nipkow 2000-07-07 Tightened up check of types in constant defs.
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-04-17 wenzelm 2000-04-17 name space hide operations;
1999-07-12 wenzelm 1999-07-12 removed merge_theories;
1999-05-17 wenzelm 1999-05-17 prep_ext exported (again);
1999-05-04 wenzelm 1999-05-04 hide prep_ext, merge_theories;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-03-17 wenzelm 1999-03-17 added assert_super;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-02-03 wenzelm 1999-02-03 added is_draft; renamed sig to PRIVATE_THEORY;
1998-11-17 wenzelm 1998-11-17 Theory.apply replaced by Library.apply;
1998-11-14 wenzelm 1998-11-14 val copy: theory -> theory;
1998-11-09 wenzelm 1998-11-09 removed local_theory;
1998-10-13 wenzelm 1998-10-13 PRIVATE sig parts;
1998-06-20 wenzelm 1998-06-20 added read_def_axm;
1998-06-10 wenzelm 1998-06-10 tuned comments;
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;
1998-05-28 wenzelm 1998-05-28 fixed error msgs;
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-05-12 wenzelm 1998-05-12 fixed comment;
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);
1998-04-04 wenzelm 1998-04-04 added local_theory (for Isar); added setup;
1998-02-12 wenzelm 1998-02-12 Sign.merge vs. Sign.nontriv_merge;
1998-02-12 wenzelm 1998-02-12 tuned add_trrules;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;
1997-12-02 wenzelm 1997-12-02 tuned trfuns types;
1997-11-20 wenzelm 1997-11-20 init_data: improved print method;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-05 wenzelm 1997-11-05 adapted add_trfunsT; defs: admit TYPE arguments;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-10-30 wenzelm 1997-10-30 tuned init_data;
1997-10-28 wenzelm 1997-10-28 added ancestors;
1997-10-24 wenzelm 1997-10-24 tuned names; tuned prep_ext_merge;