generalized type of hyperpow; removed hcpow

redefine hSuc as *f* Suc, and move to HyperNat.thy

proper use of IntInf instead of InfInf;

defs/notes: more robust transitivity reasoning;

added trans_terms/props;

locale: print context for begin;

remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq

remove uses of star_n and FreeUltrafilterNat

remove use of FreeUltrafilterNat

added lemmas about hRe, hIm, HComplex; removed all uses of star_n

fixed type

added stub for OCaml serializer

cleanup

whitespace correction

clarifed comment

dropped FIXME comment

clarified character setup

remove references to star_n

SComplex abbreviates Standard

simplified mk/dest_numeral (cf. mk/dest_binum of 1.65); put signature into canonical order;

removed legacy ML bindings;

updated;

tuned signature;

internal_abbrev: observe print mode;

target_abbrev: internal mode for abbrevs; tuned;

edge: actually apply operation!

tuned;

authentic syntax for number_of

introduced mk/dest_numeral/number for mk/dest_binum etc.

fixed syntax for bounded quantification

dropped superfluous header

clarified error message

nat type now has a size functin => no longer needed as special case

simplified

local_abbrev: proper fix/declare of local entities;

Deleted the unused type argument of UVar

tuned comments;

added IsarAdvanced/Functions

generalized some lemmas; removed redundant lemmas; cleaned up some proofs

remove uses of scaleR infix syntax; add lemma Reals_number_of

tuned;

add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);

updated;

simplified unlocalize_mixfix;

removed is_class -- handled internally; begin: is_class argument; added fork_mixfix; abbrev/defs: internal_abbrev produces hypothetical term;

notation: Term.equiv_types; add_abbrev: tuned signature, added assumption export; added local_abbrev; tuned;

abbrev: tuned signature;

tuned expand_term;

classified show/thus as prf_asm_goal, which is usually hilited in PG;

tuned expand_binds;

tuned error messages;

added equiv_types;

add_abbrev: tuned signature;

added expand_term_frees;

abbreviate: tuned signature;

LocalTheory.abbrev;

removed redundant constants and lemmas

additions to HOL-Complex

Removal of the "keep_types" flag: we always keep types!

make SML/NJ happy;

made SML/NJ happy;

consistent naming for FreeUltrafilterNat lemmas; cleaned up

cleaned up; generalized some proofs

fix assumptions on NSDERIV_quotient

changed (ns)deriv to take functions of type 'a::real_normed_field => 'a

generalize some theorems

add type annotation

read_xnum: return leading_zeros, radix;

authentic syntax for Pls/Min/Bit; separated translation functions from HOLogic functionality;

authentic syntax for Pls/Min/Bit;

binary numerals: restricted to actual abstract syntax; tuned;

Hyperreal/FrechetDeriv.thy

theory of Frechet derivatives

specials: include single quote;

xstr: disallow backslashes;

advanced translation functions: Proof.context; abs/binder_tr: disallow internal names for bounds;

advanced translation functions: Proof.context;

added improved versions of use_text/file (still inactive);

added use_file;

load secure.ML after symbol.ML, when default output is active;

ordered lists instead of tables for resolving hyps; speedup

nominal_primrec now prints initial proof state.

Abbreviations can now be specified simultaneously with introduction rules.

Adapted to new inductive definition package.

added ProofGeneral settings;

tuned comments;

tuned;

defs: increased entropy of mixfix handling;

fixed term_of_list;

Concrete syntax for hex chars and strings.

renamed str_of_XXX to print_XXX;

HOLogic cleanup;

ML_Syntax.print_XXX;

misc cleanup -- removed non-HOL operations; nibble/char/list/string: observe conventions for abstract syntax operations;

moved char/string syntax to Tools/string_syntax.ML; HOLogic cleanup;

added Tools/string_syntax.ML; tuned;

removed junk;

interpretation: use C_class name prefix;

abs/binder_tr': support printing of idtdummy;

respects2: tuned spacing;

support printing of idtdummy;

added is_class (approximation); added abbrev; tuned;

LocalTheory.notation/abbrev;

extract_case: Name.clean;

added target_notation/abbrev; tuned;

added notation/abbrev (from term_syntax.ML);

tuned absdummy;

added no_frees; add_abbrev: tuned handling of frees, temp workaround;

removed (cf. proof_context.ML and local_theory.ML);

removed Isar/term_syntax.ML;

avoid internal name O_;

hide const linorder.less_eq_less.max linorder.less_eq_less.min;