updated generated file;

use underscore for underscore;

output_entity: added \mbox{} to prevent hyphenation;

added more infrastructure for fresh_star

added mising lemma

Added documentation

moved begin and imports to ../isar.sty;

added begin and imports;

clean_string: handle { };

converted pure.tex to Thy/pure.thy;

polished the proof for atm_prm_fresh and more lemmas for fresh_star

unfold_locales part of default method.

extended to be a library of general facts about the lambda calculus

tuned some proofs and comments

added lemma antiquotation

proper input abbreviations in class

replaced various macros by antiquotations; misc tuning;

more ref macros;

session based on HOL;

thms Max_ge, Min_le: dropped superfluous premise

proper command/keyword markup;

added AND, IS, WHERE symbols;

converted syntax.tex to Thy/syntax.thy;

dropping return in imperative monad bindings

corrected ML semantics

added setup for Isar entities; tuned;

fixed recdef, broken by my previous commit

* New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size

Merged theories about wellfoundedness into one: Wellfounded.thy

moved 'trivial classes' to foundation of code generator

tuned index commands;

more abstract index commands;

added \indexoutersyntax; removed permuted index;

fixed proof

misc cleanup;

converted intro.tex to Thy/intro.thy;

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.