Merge

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

merged

added proof method rewrite

merged

tuned;

tight span for theory header, which is relevant for error positions (including semantic completion);

misc tuning and simplification;

Inserted real_of_nat to fix factorial-related problem

more general type class for factorial. Now allows code generation (?)

Merge

Merge

The factorial function, "fact", now has type "nat => 'a"

merged

added lemmas

document property

BNF relators preserve reflexivity

export more ML functions

merged

suppress semantic completion in errors of batch build -- avoid junk in log files;

updated docs

clarified documentation

proper headers;

merged

tuned message -- include completion;

support for completion reports produced in Scala (inlined into messages);

more precises positions; more permissive imports;

avoid duplicate header errors, more precise positions; tuned signature;

tuned protocol -- resolve command positions in ML;

clarified modules;

add inequalities (move from AFP/Amortized_Complexity)

merge

inlining threshold

avoid controversial Pirate syntax

more markup, which helps to create missing imports;

tuned signature;

proper command id for inlined errors, which is important for Command.State.accumulate;

clarified span position;

tuned;

tuned;

hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;

more command categories, as in ML; tuned;

more command categories, as in ML;

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

more explicit exception User_Error, with value-oriented equality;

tuned signature;

clarified positions of theory imports;

misc tuning -- more uniform ML vs. Scala;

tunes signature -- more uniform ML vs. Scala;

position parser as in ML;

tuned signature; minimal I/O on GUI thread should be OK;

rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;

removed junk;

tuned;

merged

clarified markup for embedded files, early before execution;

clarified command content;

tuned -- more uniform ML vs. Scala;