Added xml_syntax.ML

Added Tools/xml_syntax.ML

circumvented defect in SML/NJ type inference

1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given.

removed division_by_zero class requirements from several lemmas

added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas

choose gnuplot terminal by platform

set terminal png color -- works for older versions of gnuplot;

added ZF-UNITY;

tidied

Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.

make it work on sunbroy2

Moved the functional equality axioms to helper1 files.

Introduced combinators B', C' and S'.

Removed include_min_comb and include_combS.

Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.

improvements for codegen 2

name shifts

fixed bug

Removed "induct set" attribute from total induction rules

removed debug

Fixed error in pattern splitting algorithm

change section to subsection

add header

renamed axclass_xxxx axclasses;

tuned;

added standard;

added name_classrel/arities/arity;

pretty_full_theory: suppress internal entities by default;

Logic.name_classrel/arities;

revert to previous version;

added General/susp.ML;

removed duplicate arities;

sko/abs: Name.internal prevents choking of print_theory;

tuned method setup;

tuned proofs;

'print_theory': bang option for full verbosity;

* Pure: 'print_theory' now suppresses entities with internal name;

tuned;

simple html output;

timespan: 100 days;

superceded by isatest-statistics;

tuned;

target dir; proper time formats;

Standard statistics.

time: include year;

Produce statistics from isatest session logs.

moved Import/susp.ML to Pure/General;

renamed axclass_xxxx axclasses

removed diagnostic messages

Operational Equality

this file contains a compile-challenge suggested by Adam Chlipala; so far it contains only the definition and no proofs

tuned

added auxiliary lemma for code generation 2

removed

moved part of normalization oracle here

classical arity syntax

added codegen_data

moved base setup for evaluation oracle hier

added OperationalEquality.thy

code generation 2 adjustments

(void)

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