src/Pure/pure_thy.ML
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-20 wenzelm 2001-11-20 trfuns *after* binder syntax;
2001-11-19 berghofe 2001-11-19 Further restructuring of theorem naming functions.
2001-11-11 wenzelm 2001-11-11 renamed open_smart_store_thms to smart_store_thms_open; added Syntax.pure_syntax_output;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-10-31 berghofe 2001-10-31 - enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments
2001-09-28 wenzelm 2001-09-28 internal thm numbering with ":" instead of "_";
2001-08-31 berghofe 2001-08-31 Added equality axioms and initialization of proof term package.
2000-12-13 wenzelm 2000-12-13 eliminated GOAL syntax;
2000-11-12 wenzelm 2000-11-12 Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-09-02 wenzelm 2000-09-02 added get_thm_closure;
2000-08-09 wenzelm 2000-08-09 added get_thms_closure, single_thm;
2000-08-04 wenzelm 2000-08-04 dummy_pattern moved to term.ML;
2000-07-13 wenzelm 2000-07-13 add_defs(_i): overloaded option;
2000-07-04 wenzelm 2000-07-04 added "nothing" (empty list of theorems);
2000-07-01 wenzelm 2000-07-01 print_theorems: omit name space;
2000-06-29 wenzelm 2000-06-29 have_thmss: handle multiple lists of arguments;
2000-05-31 wenzelm 2000-05-31 get_thm(s): automatic transfer;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-03-13 wenzelm 2000-03-13 add_thms, add_axioms, add_defs: return theorems as well;
1999-11-29 wenzelm 1999-11-29 Goal: tuned pris;
1999-10-27 wenzelm 1999-10-27 dummy_pattern: aprop;
1999-10-21 wenzelm 1999-10-21 forall_elim_var(s) move here from drule.ML; add_axioms/defs: forall_elim_vars on result;
1999-10-08 wenzelm 1999-10-08 theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
1999-10-06 wenzelm 1999-10-06 fixed naming of single axioms;
1999-09-06 wenzelm 1999-09-06 removed thms_closure (unused);
1999-09-04 wenzelm 1999-09-04 eliminated default_name (thms no longer stored for name "");
1999-09-01 wenzelm 1999-09-01 smart_store_thms;
1999-08-19 wenzelm 1999-08-19 tuned Goal syntax;
1999-07-12 wenzelm 1999-07-12 thms_containing: undeclared consts error;
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-06-04 wenzelm 1999-06-04 fixed BUG in have_thmss: return thy';
1999-05-21 wenzelm 1999-05-21 avoid string constants;
1999-05-21 wenzelm 1999-05-21 backup replaced by checkpoint;
1999-05-17 wenzelm 1999-05-17 backup operation replaces transaction;
1999-05-04 wenzelm 1999-05-04 transaction: Theory.copy;
1999-05-01 wenzelm 1999-05-01 renamed 'dummy' to 'dummy_pattern' (less dangerous);
1999-04-30 wenzelm 1999-04-30 theory data: copy; consts dummy :: 'a ("'_");
1999-03-17 wenzelm 1999-03-17 added cond_extern_thm_sg; have_thmss: name made optional;
1999-03-11 wenzelm 1999-03-11 workaround default_name problem;
1999-01-12 wenzelm 1999-01-12 tuned signature;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
1998-11-19 wenzelm 1998-11-19 no warning for "it" theorems;
1998-11-17 wenzelm 1998-11-17 added default_name; added have_tthmss;
1998-11-16 wenzelm 1998-11-16 Attribute.thms_of;
1998-10-20 wenzelm 1998-10-20 Symtab.foldl;
1998-08-17 wenzelm 1998-08-17 added get_tthmss;
1998-08-06 wenzelm 1998-08-06 added store_tthm;
1998-07-28 wenzelm 1998-07-28 removed global_names flag;
1998-07-22 wenzelm 1998-07-22 moved long_names / cond_extern to name_space.ML;
1998-06-29 wenzelm 1998-06-29 tuned transaction; moved actual (C)Pure theories to pure.ML;
1998-06-17 nipkow 1998-06-17 Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
1998-06-10 wenzelm 1998-06-10 tuned transaction;
1998-06-10 wenzelm 1998-06-10 moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;
1998-06-08 wenzelm 1998-06-08 use type-safe theory data interface;
1998-06-05 wenzelm 1998-06-05 added print_theorems: theory -> unit; added print_theory: theory -> unit; added transaction mechanism as last resort to accomodate non-atomic transformers (please avoid such things); tuned setup;
1998-05-25 wenzelm 1998-05-25 added get_name, put_name, global_path, local_path, begin_theory, end_theory;
1998-05-15 wenzelm 1998-05-15 added add_axioms_x, add_defs_x;