updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;

brought up to date with TPTP_Proof;

using richer annotation from formula annotations in proof;

extracting more info from formula annotation in proof;

corrected syntax filter;

reading tptp status code;

improved handling of nonstandard problem names;

merged

merged

tuned proofs -- less guessing;

cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;

minor tuning;

cases: more position information and PIDE markup;

more liberal 'case' syntax: allow parentheses without arguments;

more robust ToyList_Test;

Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);

tuned proofs -- clarified flow of facts wrt. calculation;

proper imports; tuned proofs;

tuned proof;

more explicit indication of 'guess' as improper Isar (aka "script") element;

Further clarifies sublocale and rewrite morphisms.

Clarifies that interpretation does not only apply to facts, but to declaratoins in general.

Clarifies documentation of interpretation in local theories.

New test case: interpretation in named contexts is not persistent.

Terminology: mixin -> rewrite morphism.

merged

added lemmas

merged