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

New theory SupInf of the supremum and infimum operators for sets of reals.

eliminated hard tabulators, guessing at each author's individual tab-width;

tuned initial session setup;

merged

proper headers;

reactivated sun-poly, as parallel test;

merged

merged

merged