proof endings: no Toplevel.print!

all_valid_thms: use new facts tables;

Theory.subthy;

Facts.intern, Facts.extern_table;

IsarCmd.hide_names;

added hide_names command (formerly Sign.hide_names), support fact name space;

Facts.dest_table, PureThy.facts_of;

simplified hide_XXX interfaces;

removed obsolete SIGN_THEORY -- no name aliases in structure Theory; removed obsolete BASIC_THEORY;

removed obsolete SIGN_THEORY -- no name aliases in structure Theory; simplified hide_XXX interfaces; moved hide_names to isar_cmd.ML;

added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;

Theory.eq_thy;

renamed dest to dest_table, and extern to extern table; added name space intern/extern;

PureThy.hide_fact;

Facts.dest_table;

Sign.hide_const;

added hide fact;

tuned;

removed eval_antiquotes_fn; eval: CRITICAL for now;

merge: canonical order;

Library.is_equal;

moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;

disallow duplicate entries (weak version for merge); added hide;

Thm.forall_elim_var(s);

proper dynamic facts for eqvts, freshs, bijs; removed obsolete print_data -- facts are accesivle via regular names; misc tuning/simplification;

overloading perm: use big_name; avoid rebinding of perm_closed -- leftover debug code;

* Name space merge now observes canonical order; * Authentic naming of facts;

removed redundant hd_append variant;

removed duplicate lemmas;

avoid duplicate fact bindings;

overloading of perm: adhoc name prevents duplicate fact names;

Changed naming scheme for theorems generated by interpretations.

proper context for induct_scheme method

Isar.toplevel_loop: separate init/welcome flag;

Sorts.class_error: produce message only (formerly msg_class_error);

tsig: removed unnecessary universal witness; Sorts.class_error: produce message only (formerly msg_class_error);

simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;

removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;

added insert_sorts (from thm.ML);

tsig: removed unnecessary universal witness;

tuned;

removed unnecessary Goal.close_result;

replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); pred_def: tag internal;

advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);

added is_utf8_trailer;

rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;

obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;

removed obsolete compress.ML

replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

rep_cterm/rep_thm: no longer dereference theory_ref;

use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;

transaction/init: ensure stable theory (non-draft);

export is_draft, not draftN;

simplified isarcmd;

eliminated unused name_of, source, source_of, print', print3, three_buffersN; tuned;

eliminated unused trace, read;

eliminated unused Toplevel.print3/three_buffers;

tuned;

Isar.goal: tactical goal only;

eliminated backpatching of load_thy;

added read_const_exprs (from Pure/Isar/code_unit.ML);

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;

ThyInfo.get_names;

ThyInfo.get_theory;

export load_thy -- no backpatching;

export subst_alias; moved read_const_exprs to Tools/code_package.ML -- avoids dependency on ThyInfo;

load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;

val theory = ThyInfo.get_theory;

replaced Isar loop variants by generic toplevel_loop;

replaced Isar loop variants by generic toplevel_loop; eliminated obsolete get_interrupt (subsumed by crash handling);

The global Isabelle/Isar state and main read-eval-print loop.

replaced Isar.toplevel by Toplevel.program;

moved global Toplevel state to structure Isar;

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;

finish: removed unnecessary Isar.init;

moved structure Isar to isar.ML; added type isar (from toplevel.ML);

Context.set_thread_data: non-critical;

added Isar/isar.ML;

improvements are strict

check validity of class target improvement

print_consts only for external specifications;

fundef_afterqed: removed unused config, added do_print flag; print_consts only for external specifications;

minimal error handling;

replaced ML by ML_val;

avoid control symbols in document (\<^fixed>);

\usepackage[english]{babel} (required for guillemots);

renamed mbind to scomp

removed syntax from monad combinators; renamed mbind to scomp

rudimentary user-syntax for terms

fix spelling

fix spelling

move lemmas from Word/BinBoolList.thy to List.thy

fixed makefiles

added missing file

tuned;