*** empty log message ***

*** empty log message ***

The HOL tutorial.

moved images to gfx dir;

tuned;

SYNC;

emacs local vars;

emacs local vars; added conversions (Simplifier.rewrite etc.); updated tracing example; fixed theory setup;

added nonterminals, setup; removed print_data;

added Antiquote example;

mkdir -p;

emacs local vars; isatool install;

SYNC;

emacs local vars;

isatool install;

install binaries with absolute references to ISABELLE_HOME/bin;

debugged split_eta_proc

tidied

Tidying

New UNITY files

New theory Lift

new theorems

tidied

new theorems; adds [le_refl, less_imp_le] as simprules

adjusted for new rewrites

tidied

tidied

Must remove leD from simpset

tidied

Must remove less_imp_le from simpset

Added converse_rtranclE(2)

Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm

fixed param;

assume: adjust_maxidx;

new version, more resistant to PROOF FAILED. Now it distinguishes between inferences that update the branch (resolve_tac) and those that do not (match_tac)

The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.

new theorem zero_less_diff

Misc changes

Deleted obsolete declaration of PartE'

Tidied, removing uses of less_imp_diff_positive

tidied

fixed overloading of "image"

Overloading decl should assist Blast_tac

less_imp_diff_positive is redundant with new simprule zero_less_diff

Some new theorems. zero_less_diff replaces less_imp_diff_positive

ZF.thy

new theorem Un_Diff_Int

added comment

new theorem diff_Suc_less_diff

added get_tthmss;

Mention RegExp2NA.

expandshort

Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy contains fewer theorems than before

Now allows "." in rule names, with special treatment for "be"

Direct translation RegExp -> NA!

Additions to Lex.

got rid of some goal thy commands

now trans_tac is part of the claset...

Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML

expandshort

Uses Goal instead of "goal...thy" to avoid theory problems

even more tidying of Goal commands

tidying

Moved the definition of s_u (as s) into the locale

Constrains, Stable, Invariant...more of the substitution axiom, but Union does not work well with them

simpler SELECT_GOAL no longer inserts a dummy parameter

Rule mk_triv_goal for making instances of triv_goal

Blast_tac is faster

stac now handles definitions as well as equalities

stac

minor adaption for SML/NJ

added theorems Id_o, o_Id corrected name of theorem: fund_upd_other -> fun_upd_other

cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML

the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset

renamed mk_meta_eq to meta_eq

removed superfluous o_apply

streamlined proofs with new hoare_conseq1, hoare_conseq2

defined map_upd by translation via fun_upd changed syntax of map_upd to be consistent with that of fun_upd added chg_map, map_upds

added Eps_eq

removed use_thys implied by use_thy "Main"

repaired proof of chfindom_monofun2cont

added length_Suc_conv, finite_set

replaced idt by pttrn in @filter

replaced split_etas by split_eta_proc

added ospec AddIffs [elem_o2s]

minor correction: n must not be used as free variable

eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun

suffix, unsuffix moved to Pure/library.ML;

fixed comment;

tuned;

??id syntax for text variables;

dest_binding, dest_skolem;

val single: 'a -> 'a list; val suffix: string -> string -> string; val unsuffix: string -> string -> string;

Tidying of AC, especially of AC16_WO4 using a locale

More lemmas about lex.

*** empty log message ***

List now contains some lexicographic orderings.

added store_tthm;

Improved well-formedness check.

even more tidying of Goal commands

A higher-level treatment of LeadsTo, minimizing use of "reachable"

Simplified proof!!

*** empty log message ***

Lemma renamed in HOL.

Added macro `termi'

New lemmas in List and Lambda in IsaMakefile

Removed duplicate thms (see comment to Arith.ML)

Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1

Removed comments.

even more tidying of Goal commands

disjointness

Now recognizes both {}= and ={}

Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)

New result from AC directory

added solve_tac;

New results from AC

First steps towards termination of simply typed terms.

binding / skolem vars;

Null program and a few new results

Finished the example