proper type for fun/arg_cong_rule;

added fun/arg_cong_rule;

unified names: foo_conv;

tuned;

added fun flip f x y = f y x

generalize setsum lemmas from semiring_0_cancel to semiring_0

tuned proofs;

bang_facts: warning;

tuned proofs;

(class target)

cleaned up

beta/eta conversion after preprocessor

fixed typo

more conversions; tuned;

Moved extraction_expand declaration of listall_def outside of definition.

Adapted to new naming scheme for definitions.

Changed name of raw definition.

Name of ML function "not" is now qualified in order to avoid clashes with names of constants introduced by the user.

consts in consts_code Isar commands are now referred to by usual term syntax

size [nat] is identity

explicit import of Datatype.thy due to hook bootstrap problem

localized Sup/Inf

localized Min/Max

tuned

fix proofs

remove redundant lemmas

lemmas iszero_(h)complex_number_of are no longer needed

instance real_algebra_1 < ring_char_0

new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas

moved conversions to structure Conv; get_axiom_i;

added dest_fun/fun2/arg1; removed dest_binop; renamed cterm_(fo_)match to (fo_)match; renamed cterm_incr_indexes to incr_indexes_cterm;

tuned argument_type_of;

added destructors from drule.ML; added mk_binop;

moved some operations to more_thm.ML and conv.ML;

Conversions: primitive equality reasoning (from drule.ML);

added conv.ML;

Thm.match;

moved some Drule operations to Thm (see more_thm.ML);

Thm.first_order_match;

moved conversions to structure Conv;

"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"

add lemma norm_diff_ineq; shorten other proofs

removed Complex/ComplexBin.thy;

tuned ML setup;

tuned syntax;

eliminated unnamed infixes;

removed unused mk_cond_defpair;

simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification); trace_simp_depth_limit_exceeded: attempt to hide destructive pointer programming within simpset;

remove empty, unused theory

remove redundant lemmas

add lemma hnorm_hyperpow

add lemma of_hypreal_hyperpow

tuned

moved recfun_codegen.ML to Code_Generator.thy

continued

remove redundant lemmas

hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas

add lemma hnorm_divide

add lemmas abs_hnorm_cancel, hnorm_of_hypreal

add lemmas norm_add_less, norm_mult_less

add lemma Standard_hyperpow

tuned;

add of_hypreal constant with lemmas

add lemmas norm_number_of, norm_of_int, norm_of_nat

quoted 'declaration';

simplified pretty_thm(_legacy);

is_sid: include '::';

tuned ProofDisplay.pretty_full_theory;

tuned;

updated;

simplified context data;

tuned;

legacy_intern_skolem: legacy_feature;

tuned;

renamed call_atp to sledgehammer;

updated;

tuned context data;

ML adaptions

clean up complex norm proofs, remove redundant lemmas

remove redundant lemmas

fix proof of hypreal_sqrt_sum_squares_ge1

add lemma real_sqrt_sum_squares_triangle_ineq

add lemma abs_norm_cancel

cleaned up

polished some proofs

add lemmas power2_le_imp_le and power2_less_imp_less

add lemma power_less_imp_less_base

clean up RealVector classes

First-order variant of the fully-typed translation

added further equality example

changed 'code nofunc' to 'code func del'

* Context data interfaces;

simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;

simplified DataFun interfaces;

changed code generator invocation syntax

PreList imports RecDef

dropped legacy ML binding

added auxiliary lemmas for proof tools

dropped preorders, unified syntax

minimal import

dropped HOL.ML

tuned

updated Alice version;

IntInf.fromInt;

added "set" supression

added test about "set" supression

polished all proofs and made the theory "self-contained"

deleted some unnecessary type-annotations

tuned some of the proofs and added the lemma fresh_bool

tuned allpairs

tuned some proofs and changed variable names in some definitions of Nominal.thy

added allpairs

removed obsolete get_sg;

explicit treatment of legacy_features;

Fixing bugs in the partial-typed and fully-typed translations

Removal of dead code

tuned some proofs in CR and properly included CR_Takahashi

removed obsolete induct/simp tactic;

alternative and much simpler proof for Church-Rosser of Beta-Reduction

use correct email program for sunbroy2

removed legacy ML files;

eliminated unnamed infixes;

added header;

added header; tuned presentation;

added

removed lagacy ML files;

updated;

eliminated unnamed infixes;