introduced abstract view on number expressions in hologic.ML

whitespace fix

added code generation syntax for some char combinators

infix syntax for generated code for composition

new-style oracle setup

added functions tutorial

Add abstraction for objtypes and documents.

removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy

moved several theorems; rearranged theory dependencies

hypreal_of_hypnat abbreviates more general of_hypnat

tracing instead of warning

updated;

removed obsolete assert;

renamed LocalTheory.assert to affirm;

tuned -- accomodate Alice;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

remove Hyperreal/fuf.ML

remove commented section

remove ultra tactic and redundant FreeUltrafilterNat lemmas

declare insert_iff [simp]

activated improved use_ml, which captures output and reports source positions; define use_file in terms of use_ml;

tuned;

prove hyperpow_realpow using transfer

remove usage of ultra tactic

add lemmas singleton and insert_iff

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;