simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output

merged

adjusted import to changed HOL theory graph

moved theory Divides after theory Nat_Numeral; tuned some proof texts

proper nested quotes; give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);

components: ensure that the last line is read, even if it lacks EOL;

updated Isar.goal;

renamed raw Proof.get_goal to Proof.raw_goal;

back to Proof.raw_goal;

renamed Proof.flat_goal to Proof.simple_goal;

Isar.goal: Proof.simple_goal, not raw version;

replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;

provide SpecParse.constdecl/constdef, e.g. for quotient_definition;

slightly more robust error message;

tuned;

merged

merged

misc tuning;

let naming transform binding beforehand -- covering only the "conceal" flag for now; export LocalTheory.standard_morphism;

tuned;

simplified default binding; conceal internal bindings;

conceal internal bindings;

Drule.store: proper binding; conceal internal bindings;

added restore_naming;

load Product_Type before Nat; dropped junk

moved lemmas for dvd on nat to theories Nat and Power

Probability tweaks

merged

New theory Probability, which contains a development of measure theory

merged