little bugfixes; added induct_thm_tac

moved to Product_Type_lemmas.ML

added translations for bind_thm and val

converted to Isar, simplifying recursion on class hierarchy

converted to Isar therory, adding attributes complete_split and split_format

converted to new-style theories;

updated

ext_classrel: certify_class;

comment

tuned

tuned;

added "numerals" theorems;

thms_containing: term args;

* Pure: 'thms_containing' now takes actual terms as arguments; * isatool convert assists in eliminating legacy ML scripts;

added sum_case_map_upd_empty, sum_case_empty_map_upd, and sum_case_map_upd_map_upd (also to default simpset), added map_of_map

debugged declare

further minor improvements

strip_blanks moved to General/symbol.ML;

pretty_text: tweak_lines handles linebreaks gracefully;

added strip_blanks;

added attribute declarations, etc.

improved theory reference in comment

added diff_single_insert and subset_image_iff

shortened proof of some1_equality

more robust handling of rule cases hints;

tuned;

added if_def2

added foldln

corrected file name suffixes

removed (obsolete) mult_assumption

Fixed bug in complete_split_rule_var.

tuned;

avoid dead code;

Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy

*** empty log message ***

*** empty log message ***

added Unix example;

updated;

*** empty log message ***

Completely split rule eval_evals_exec.induct before applying it.

New function complete_split_rule for complete splitting of partially splitted rules (as generated by inductive definition package).

Splitting of arguments of product types in induction rules is now less aggressive.

fixed the pr example

simplified gcd

fixed set comprehension print translation

Merged Example into While_Combi

*** empty log message ***

renamed to Transitive_Closure_lemmas.ML;

tuned;

Transitive_Closure turned into new-style theory;

tuned;

*** empty log message ***

added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project Verificard

* Document preparation: renamed standard symbols \<ll> to \<lless> and \<gg> to \<ggreater>;

added eufrak symbols; renamed \<ll> to \<lless> and \<gg> to \<ggreater>;

more symbols;

empty_upd_none;

debugging and extensions

*** empty log message ***

*** empty log message ***

no_brackets;

tuned;

arg_cong, tacticals, pr, defer, prefer

added HOL-Unix example;

2 to #2

the 0<n premise was unnecessary

added a "pr" example; tidied

deleted several obsolete lemmas from NatArith.ML

tidied using arith_tac

deleted obsolete theorems

tided

arg_cong example; tidying to use @subgoals

rename_tac example; tidying to use @subgoals

new examples theory Rules/Tacticals.thy

setuo indent: \isaindent;

setup indent;

added spaces; added default_indent, indent;

support general indentation (e.g. for non-tt latex output); tuned;

added replicate_string;

updated;

\isaindent;

tuned;

Ring_and_Field_Example;

instance int :: ordered_ring moved to Ring_and_Field_Example, because it changes the way that int expressions get simplified, violating the strict library principle (cf. README.html);

added Library/Ring_and_Field_Example.thy;

*** empty log message ***

added HOL/Library/Nested_Environment.thy;

updated;

more bugs;

forget RPM;

convert legacy tactic scripts to Isabelle/Isar tactic emulation;

made SML/XL happy;

tuned;

show(_i): check goal;

show/thus: check_goal;

show/thus: Toplevel.proof';

infix \\\\;

added exists_stamp; added PureN, CPureN;

use Sign.PureN, Sign.CPureN;

Sign.exists_stamp;

tuned \<And> and \<Or>;

generate index.html for pdf docs;

splitted Loop rule

removed redundant proof

is_class and class now as defs (rather than translations); corrected Digest.thy

use_output: proper handling of non-ASCII symbols;

export plain_output;

Store.thy is obsolete (newref isn't used any more)

removed obsolete MicroJava/JVM/Store.thy

newref -> new_Addr

renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats

renamed Product_Type.split to split_conv;

use Syntax.read_xnum;

tuned examples;

* HOL/datatype: induction rule for arbitrarily branching datatypes is now expressed as a proper nested rule (old-style tactic scripts may require atomize_strip_tac to cope with non-atomic premises); * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule to "split_conv" (old name still available for compatibility); * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals);

use_text etc.: proper output of error messages;

export fold_ast etc.;

removed Session.finish ();

proper induction rule for arbitrarily branching datatype;

export inductive_forall_name, inductive_forall_def, rulify;