more general evaluation combinators

different handling of eq class for nbe

basic setup for generated document (cf. ../IsarImplementation);

dropped theory PreList

added explicit check phase after reading of specification

added theory Sublist_Order

dropped some metis calls

tuned proofs

constant HOL.eq now qualified

exported is_abbrev mode discriminator

proper abbreviations in class

dropped theory PreList

added entries

move some at/a64 tests to intel mac hardware (running Linux)

updated generated file;

updated generated file;

NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;

removed dead code;

print_cases: proper context for revert_skolem;

tuned;

modernized specifications and proofs;

improved definition of upd

* Context-dependent token translations.

revert_skolem: do not change non-reversible names; default token translations: revert_skolem; removed obsolete revert_skolems;

print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);

no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);

variant_fixes: preserve internal state, mark skolem only for body mode; import_inst: actually observe is_open flag (cf. variant_fixes);

prove_global: Variable.set_body true, pass context;

adapted to ProofContext.revert_skolem: extra Name.clean required;

prove_global: pass context;

pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);

replaced token translations by common markup; use XML.text instead of separate escape;

moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;

token translations: context dependent, result Pretty.T; added Markup.fixed (analogous to Markup.const); tuned;

replaced token translations by common markup;

default token translations with proper markup;

token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;

removed obsolete raw_str; added mark;

added markup for fixed variables (local constants);

token translations: context dependent, result Pretty.T;

Pretty.mark;

unused_thms: sort_distinct;

Sign.add_path;

removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;

pretty_theorems: use proper PureThy.facts_of;

Facts.extern_static;

PureThy.defined_fact; unused_thms: simplified signature;

renamed check_fact to defined_fact;

removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;

valid_facts: more elementary version using Facts.fold_static;

Facts.dest_static;

Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.

removed unused TLA/Memory/MIParameters.thy;

removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;

removed obsolete premsN;

PureThy.get_fact: pass dynamic context;

tuned;

removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;

tuned proofs;

Added entry for unused_thms command.

Adapted to new primrec package.

Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).

educated guess for infix syntax

removed test artefacts

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;