added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;

exported master_directory;

present_excursion: setmp_thread_position during presentation;

use: explicit .ML;

ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;

fixed improper handling of return code (pdf and ps.gz formats)

add constants: set Markup.theory_nameN in tags;

added theory_nameN;

rearranged subsections

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.

Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.

temporary adjustment

tuned

more permissive preprocessor

explicit type schemes for functions

moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs

added code for quantifiers

simplified proof

made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct

use_file: added str_of_pos argument (ignored);

Added entry explaining incompatibilities introduced by replacing sets by predicates.

instantiation lift :: (countable) bifinite

use new class package for classes profinite, bifinite; remove approx class

updated generated file;

unparse_term: check PureThy.old_appl_syntax instead of CPure;

theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;

converted to regular application syntax;

eliminated theory CPure;

setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

proper handling of the return code for the ps-format (fixes a bug)

oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;

command 'normal_form': proper context via Variable.auto_fixes;

moved global pretty/string_of functions from Sign to Syntax; reordered signature;

Syntax.string_of_sort: proper context;

pprint: proper global context via Syntax.init_pretty_global;

Syntax.string_of_typ: proper context;

moved global pretty/string_of functions from Sign to Syntax; tuned message;

removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway); full_path: no link expansion here (reverted change of 1.18); ident: OS.FileSys.fullPath takes care of link expansion;

renamed type decompT to decomp; refute: proper context for trace_ex; some attempts to improve readability;

Syntax.string_of_term with proper context;

moved global pretty/string_of functions from Sign to Syntax; removed dead code;

renamed type decompT to decomp;

pr_matrix: proper context;

guess_instance: proper context;

moved global pretty/string_of functions from Sign to Syntax;

tuned comments;

tuned proofs;

avoid undeclared variables in facts;

avoid undeclared variables within proofs; refrain from setting global references;

avoid undeclared variables within proofs;

tuned proof;

avoid undeclared variables within proofs;

cat_lines;

default token translations: observe Sign.is_pretty_global for fixed variables;

added pretty_global flag;

structure Display: less pervasive operations;

rename locales; add completion_approx constant to ideal_completion locale; add new set-like syntax for powerdomains; reorganized proofs

added a lemma about existence of contexts

* Method "cases", "induct", "coinduct": removed obsolete "(open)" option; * Isar statements: removed obsolete case "rule_context";

removed obsolete option open; tuned comments;

removed unused make_simple;

removed obsolete case rule_context;

fix looping simplifier

tuned;

tuned comment;

updated version;

removed unnecessary/untrusive a4paper option;

use Isabelle sty files from Doc/;

removed obsolete \ifpdfoutput;

* Simplified pdfsetup.sty;

use Isabelle sty files from Doc/;

updated generated file;

use Isabelle sty files from Doc/;

tuned clean_name (underscore);

load color/hyperref unconditionally; renamed color darkblue to linkcolor (default value unchanged); removed obsolete thumbpdf;

removed obsolete thumbpdf;

updated generated file;

use ../isabelle.sty, ../isabellesym.sty;

depend on ../pdfsetup.sty;

default linkcolor=black;

clean_name: replace "_" by "-";

updated generated file;

fixed some Isar element markups;

linkcolor=black (less noisy text);

hyperref is always enabled (also works with xdvi, dvips); replaced darkblue by generic linkcolor; reduced verbosity;

depend on ../pdfsetup.sty;

clean_string: cover <; added clean_name; output_entity: hyperlink;

updated generated file;

updated generated file;

proper checking of various Isar elements;

added defined_command, defined_option;

added intern, defined;

added defined;

setmp_thread_data: do nothing if Output.debugging;

names_of: exclude intermediate ids -- less verbosity;