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;

renamed some old names Theory.xxx to Sign.xxx;

eliminated unnamed infixes; tuned ML setup;

added header;

eliminated unnamed infixes, tuned syntax;

clarified naming policy

clarified semantics of merge

moved stuff to Char_nat.thy

tuned

slightly tuned

replaced recdef by function

cleaned up code generator setup for int

added lemmatas

moved code generation pretty integers and characters to separate theories

updated doc

mk_const_def: Sign.intern_term (legacy);

renamed some old names Theory.xxx to Sign.xxx;

updated;

add the lemma supp_eqvt and put the right attribute

new lemma splice_length

fix sml compilation

Moved function params_of to inductive_package.ML.

Moved functions infer_intro_vars, arities_of, params_of, and partition_rules to inductive_package.ML.