src/Pure/pure_thy.ML
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;
1998-05-13 wenzelm 1998-05-13 added thms_closure: theory -> xstring -> tthm list option; added add_typedecls: (bstring * string list * mixfix) list -> theory -> theory; |> Theory.add_nonterminals Syntax.pure_nonterms;
1998-04-29 wenzelm 1998-04-29 tuned names of (add_)store_XXX functions; added attributes to add_thms, add_axioms, add_defs functions;
1998-04-04 wenzelm 1998-04-04 type_error;
1998-04-04 wenzelm 1998-04-04 added Goal_def;
1998-04-03 wenzelm 1998-04-03 added get_tthm(s), store_tthms(s); tuned;
1998-01-30 wenzelm 1998-01-30 tuned msgs;
1997-12-29 wenzelm 1997-12-29 pretty_name_space;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1997-11-20 wenzelm 1997-11-20 improved theorems print method: transfer_sg;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-11-03 wenzelm 1997-11-03 made SML/97 happy;
1997-10-30 wenzelm 1997-10-30 tuned thy_data;
1997-10-30 wenzelm 1997-10-30 tuned;
1997-10-28 wenzelm 1997-10-28 added ignored_consts, thms_containing, add_store_axioms(_i), add_store_defs(_i), thms_of; tuned pure thys;
1997-10-27 wenzelm 1997-10-27 oops;
1997-10-27 wenzelm 1997-10-27 renamed put_* to store_*;
1997-10-24 wenzelm 1997-10-24 oops, swap warnings;
1997-10-24 wenzelm 1997-10-24 Init 'theorems' data. The Pure theories.