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);
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness;
2008-04-13 wenzelm 2008-04-13 tuned;
2008-04-12 wenzelm 2008-04-12 removed unnecessary Goal.close_result;
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); pred_def: tag internal;
2008-04-12 wenzelm 2008-04-12 advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
2008-04-12 wenzelm 2008-04-12 added is_utf8_trailer;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
2008-04-12 wenzelm 2008-04-12 obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
2008-04-12 wenzelm 2008-04-12 removed obsolete compress.ML
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 wenzelm 2008-04-10 use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-04-10 wenzelm 2008-04-10 transaction/init: ensure stable theory (non-draft);
2008-04-10 wenzelm 2008-04-10 export is_draft, not draftN;
2008-04-10 wenzelm 2008-04-10 simplified isarcmd;
2008-04-10 wenzelm 2008-04-10 eliminated unused name_of, source, source_of, print', print3, three_buffersN; tuned;
2008-04-10 wenzelm 2008-04-10 eliminated unused trace, read;
2008-04-10 wenzelm 2008-04-10 eliminated unused Toplevel.print3/three_buffers;
2008-04-10 wenzelm 2008-04-10 tuned;
2008-04-10 wenzelm 2008-04-10 Isar.goal: tactical goal only;
2008-04-10 wenzelm 2008-04-10 eliminated backpatching of load_thy;
2008-04-10 wenzelm 2008-04-10 added read_const_exprs (from Pure/Isar/code_unit.ML);
2008-04-10 wenzelm 2008-04-10 export get_names (formerly names); moved pervasive theory = ThyInfo.get_theory to pure_setup.ML; removed unused pretty_theory; use OuterSyntax.load_thy instead of backpatched ThyLoad.load_thy;
2008-04-10 wenzelm 2008-04-10 ThyInfo.get_names;
2008-04-10 wenzelm 2008-04-10 ThyInfo.get_theory;
2008-04-10 wenzelm 2008-04-10 export load_thy -- no backpatching;
2008-04-10 wenzelm 2008-04-10 export subst_alias; moved read_const_exprs to Tools/code_package.ML -- avoids dependency on ThyInfo;
2008-04-10 wenzelm 2008-04-10 load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;
2008-04-10 wenzelm 2008-04-10 val theory = ThyInfo.get_theory;
2008-04-10 wenzelm 2008-04-10 replaced Isar loop variants by generic toplevel_loop;
2008-04-10 wenzelm 2008-04-10 replaced Isar loop variants by generic toplevel_loop; eliminated obsolete get_interrupt (subsumed by crash handling);
2008-04-10 wenzelm 2008-04-10 The global Isabelle/Isar state and main read-eval-print loop.
2008-04-10 wenzelm 2008-04-10 replaced Isar.toplevel by Toplevel.program;
2008-04-10 wenzelm 2008-04-10 moved global Toplevel state to structure Isar;
2008-04-10 wenzelm 2008-04-10 made purely value-oriented, moved global state to structure Isar (cf. isar.ML); export toplevel, error_msg (formerly print_exn), transition (formerly apply); moved type isar to structure OuterSyntax; moved crashes to structure Isar;
2008-04-10 wenzelm 2008-04-10 finish: removed unnecessary Isar.init;
2008-04-10 wenzelm 2008-04-10 moved structure Isar to isar.ML; added type isar (from toplevel.ML);
2008-04-10 wenzelm 2008-04-10 Context.set_thread_data: non-critical;
2008-04-10 wenzelm 2008-04-10 added Isar/isar.ML;
2008-04-10 haftmann 2008-04-10 improvements are strict
2008-04-10 haftmann 2008-04-10 check validity of class target improvement
2008-04-09 wenzelm 2008-04-09 print_consts only for external specifications;