changing operations for accessing data to work with contexts

removed unnecessary Thm.transfer in the predicate compiler

changing compilation to work only with contexts; adapting quickcheck

removing unused argument in print_modes function

moving towards working with proof contexts in the predicate compiler

improved values command to handle a special case with tuples and polymorphic predicates more correctly

improved behaviour of defined_functions in the predicate compiler

move some example files into new HOLCF/Tutorial directory

remove redundant hdvd relation

remove unnecessary constant Fixrec.bind

add section about fixrec definitions with looping simp rules

more informative error message for fixrec when continuity proof fails

determine margin just before rendering -- proper reformatting when updating;

simplified alignment via FlowPanel; tuned;

more systematic treatment of physical document wrt. font size etc.; eliminated (crude) double buffering; tuned;

tuned;

general Isabelle_System.try_read;

explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];

inverted "Freeze" to "Follow", which is the default; update unconditionally;

basic controls to freeze/update prover results;

show fully detailed protocol messages;

some updates following src/Tools/jEdit/dist-template/settings;

spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term

merged

dropped legacy_unconstrainT

new version of triv_of_class machinery without legacy_unconstrain

merge

added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets

remove several redundant lemmas about floor and ceiling

merged

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

simplify proof

simplify proof

remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

prefer structure Keyword and Parse;

merged

merged

remove simp attribute from square_eq_1_iff

merged

make sure chained facts don't pop up in the metis proof

fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably

generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process

identify common SPASS error more clearly

remove simp attribute from power2_eq_1_iff

dropped old Library/Word.thy and toy example ex/Adder.thy

dropped old Library/Word.thy and toy example ex/Adder.thy

do not open Legacy by default;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;

tuned;

tuned signature;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

centralized legacy aliases;

prefer structure Parse_Spec;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;

refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;

renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

renamed Outer_Parse to Parse (in Scala);

renamed Outer_Keyword to Keyword (in Scala);

avoid open Conv;

less pervasive names from structure Thm;

less pervasive names from structure Thm;