improved numeral handling for nbe

added suspensions in Pure

added some stuff for code generation 2

dropped error-prone code generation 2 for wfrec

text cleanup

introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy

explicit divmod algorithm for code generation

added operational equality

added section on code generation 2

code_gen now peek keyword

cleanupdiff

added classes real_div_algebra and real_field; added lemmas

add Real/RealVector.thy

* Pure: 'class_deps' command visualizes the subclass relation;

added class_deps;

added dest_arg, i.e. a tuned version of #2 o dest_comb;

Thm.dest_arg;

Present.display_graph;

added display_graph (from thm_deps.ML);

output: uninterpreted raw symbols -- these are usually LaTeX macros;

pretty_thm: graceful treatment of ProtoPure.thy;

added class_deps;

classes: maintain serial number;

tuned;

isatool browser: renamed option -d to -c (cf. isatool tool)

PRIVATE_FILE: slightly more robust way to create and dispose;

renamed option -d to -c (cf. isatool display); operate on PRIVATE_FILE;

updated;

Bug fix to prevent exception dest_Free from escaping

Added the max_new parameter, which is a cap on how many clauses may be admitted per round. Also various tidying up.

replaced implodeable_Ext by set_like

Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n) instead of only ... = xs!n.

replace (x + - y) with (x - y)

add type constraint to otherwise looping iff rule

generalize type of (NS)LIM to work on functions with vector space domain types

norm_one is now proved from other class axioms

removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants

hcmod abbreviates hnorm :: hcomplex => hypreal

complex_of_real abbreviates of_real::real=>complex; cmod abbreviates norm::complex=>real; removed several redundant lemmas

add instance for real_algebra_1 and real_normed_div_algebra

add instances for real_vector and real_algebra

define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals

int_diff_cases moved to Integ/IntDef.thy

generalized types of many constants to work over arbitrary vector spaces; modified theorems using Rep_star to eliminate existential quantifiers

add theorem norm_diff_triangle_ineq

add required type annotation

removed type aliases for theory/theory_ref;

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

tuned;

rrule: maintain 'extra' field for rule that contain extra vars outside elhs; rewrite_rule_extra_vars: tuned; rewritec: omit incr_indexes in most cases, which is a big performance gain;

instantiate: omit has_duplicates check, which is irrelevant for soundness;

trivial whitespace change

tuned;

more on theorems;

generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space

add instance for class division_ring

removed duplicate lemmas

fixed syntax clash with Real/RealVector

*** empty log message ***

Function package: Outside their domain functions now return "arbitrary".