2008-04-16 wenzelm 2008-04-16 removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;
2008-04-16 wenzelm 2008-04-16 pretty_theorems: use proper PureThy.facts_of;
2008-04-16 wenzelm 2008-04-16 Facts.extern_static;
2008-04-16 wenzelm 2008-04-16 PureThy.defined_fact; unused_thms: simplified signature;
2008-04-16 wenzelm 2008-04-16 renamed check_fact to defined_fact;
2008-04-16 wenzelm 2008-04-16 removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;
2008-04-16 wenzelm 2008-04-16 valid_facts: more elementary version using Facts.fold_static;
2008-04-16 wenzelm 2008-04-16 Facts.dest_static;
2008-04-16 berghofe 2008-04-16 Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.
2008-04-16 wenzelm 2008-04-16 removed unused TLA/Memory/MIParameters.thy;
2008-04-16 wenzelm 2008-04-16 removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;
2008-04-16 wenzelm 2008-04-16 removed obsolete premsN;
2008-04-16 wenzelm 2008-04-16 PureThy.get_fact: pass dynamic context;
2008-04-16 wenzelm 2008-04-16 tuned;
2008-04-16 wenzelm 2008-04-16 removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;
2008-04-16 wenzelm 2008-04-16 tuned proofs;
2008-04-16 berghofe 2008-04-16 Added entry for unused_thms command.
2008-04-16 berghofe 2008-04-16 Adapted to new primrec package.
2008-04-16 berghofe 2008-04-16 Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
2008-04-16 haftmann 2008-04-16 educated guess for infix syntax
2008-04-16 urbanc 2008-04-16 removed test artefacts
2008-04-15 wenzelm 2008-04-15 proof endings: no Toplevel.print!
2008-04-15 wenzelm 2008-04-15 all_valid_thms: use new facts tables;
2008-04-15 wenzelm 2008-04-15 Theory.subthy;
2008-04-15 wenzelm 2008-04-15 Facts.intern, Facts.extern_table;
2008-04-15 wenzelm 2008-04-15 IsarCmd.hide_names;
2008-04-15 wenzelm 2008-04-15 added hide_names command (formerly Sign.hide_names), support fact name space;
2008-04-15 wenzelm 2008-04-15 Facts.dest_table, PureThy.facts_of;
2008-04-15 wenzelm 2008-04-15 simplified hide_XXX interfaces;
2008-04-15 wenzelm 2008-04-15 removed obsolete SIGN_THEORY -- no name aliases in structure Theory; removed obsolete BASIC_THEORY;
2008-04-15 wenzelm 2008-04-15 removed obsolete SIGN_THEORY -- no name aliases in structure Theory; simplified hide_XXX interfaces; moved hide_names to isar_cmd.ML;
2008-04-15 wenzelm 2008-04-15 added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;
2008-04-15 wenzelm 2008-04-15 Theory.eq_thy;
2008-04-15 wenzelm 2008-04-15 renamed dest to dest_table, and extern to extern table; added name space intern/extern;
2008-04-15 wenzelm 2008-04-15 PureThy.hide_fact;
2008-04-15 wenzelm 2008-04-15 Facts.dest_table;
2008-04-15 wenzelm 2008-04-15 Sign.hide_const;
2008-04-15 wenzelm 2008-04-15 added hide fact;
2008-04-15 wenzelm 2008-04-15 tuned;
2008-04-15 wenzelm 2008-04-15 removed eval_antiquotes_fn; eval: CRITICAL for now;
2008-04-15 wenzelm 2008-04-15 merge: canonical order;
2008-04-15 wenzelm 2008-04-15 Library.is_equal;
2008-04-15 wenzelm 2008-04-15 moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;
2008-04-15 wenzelm 2008-04-15 disallow duplicate entries (weak version for merge); added hide;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-15 wenzelm 2008-04-15 proper dynamic facts for eqvts, freshs, bijs; removed obsolete print_data -- facts are accesivle via regular names; misc tuning/simplification;
2008-04-15 wenzelm 2008-04-15 overloading perm: use big_name; avoid rebinding of perm_closed -- leftover debug code;
2008-04-15 wenzelm 2008-04-15 * Name space merge now observes canonical order; * Authentic naming of facts;
2008-04-14 wenzelm 2008-04-14 removed redundant hd_append variant;
2008-04-14 wenzelm 2008-04-14 removed duplicate lemmas;
2008-04-14 wenzelm 2008-04-14 avoid duplicate fact bindings;
2008-04-14 wenzelm 2008-04-14 overloading of perm: adhoc name prevents duplicate fact names;
2008-04-14 ballarin 2008-04-14 Changed naming scheme for theorems generated by interpretations.
2008-04-14 krauss 2008-04-14 proper context for induct_scheme method
2008-04-14 wenzelm 2008-04-14 Isar.toplevel_loop: separate init/welcome flag;
2008-04-13 wenzelm 2008-04-13 Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness; Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-13 wenzelm 2008-04-13 simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;
2008-04-13 wenzelm 2008-04-13 removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;
2008-04-13 wenzelm 2008-04-13 added insert_sorts (from thm.ML);