hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;

tuned;

use inverse, divide from basic HOL;

norm_hhf_tac;

rewrite_goal_tac moved to tactic.ML;

added rewrite_goal_tac;

added certify_tycon, certify_tyabbr, certify_const;

has_meta_prems: include "==";

store_standard_thm "norm_hhf_eq";

proper theory context for mesontest2;

inductive_rulify2 accomodates malformed induction rules;

Sign.certify_tycon, Sign.certify_const;

improved cong_definition theorems; overloaded standard operations;

simplified induction;

added axclass power (from HOL.thy);

simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);

axclass power moved to Nat.thy;

added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;

FOL_basic_ss: simprocs moved to FOL_ss;

added atomize_eq;

val atomize = thms "atomize'";

> etc

new: > and >=

rule inversion

JMB -> JMPB. Email von Johannes Pfeifroth.

updated;

fixed \title: convert "_" to "-";

tuned isabelle environment;

subgoals

*** empty log message ***

better discussion of rule induction

Thm.dest_abs now takes an additional argument.

Moved rewriting functions from Thm to MetaSimplifier.

- Moved rewriting functions to meta_simplifier.ML - dest_abs now also takes an optional variable name as an argument - beta_conversion takes additional flag as an argument. Fully reduces the term if set to true Some tuning: - tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive, transitive, beta_conversion, abstract_rule - combination: chktypes derives types of f and t from type of == instead of using fastype_of New primitives: - eta_conversion - incr_indexes: increment indexes in theorems - cterm_incr_indexes: increment indexes in cterms - cterm_match, cterm_first_order_match - rename_boundvars

moved rewriting functions from Drule to MetaSimplifier

- new theorems imp_cong and swap_prems_eq - new function dest_equals - exported strip_imp_concl - removed incr_indexes (now in Thm)

Added new file meta_simplifier.ML

Moved meta simplification stuff from Thm to MetaSimplifier.

Added type constraint in theorem "lift".

*** empty log message ***

method 'induct' now handles non-atomic goals; improved error message; option 'stripped' deprecated;

improved: 'induct' handle non-atomic goals;

make: open_parms argument;

RuleCases.make true;

added rewrite_goal_tac; resolveq_cases_tac: generalized args; tuned atomize; assm_tac: include reflexive_thm;

added typ_instance;

Sign.typ_instance;

inductive_atomize, inductive_rulify;

* Isar/HOL: method 'induct' now handles non-atomic goals; as a consequence, it is no longer monotonic wrt. the local goal context (which is now passed through the inductive cases);

tuned atomize_goal;

minor modifications for new Springer style

minor changes

auto update

*** empty log message ***

updated;

tuned method "rule" and "default";

isamarkup: handle % in input;

tuned;

misc stuff;

tuned;

proper setup of "parallel"; removed unused rules;

tuned notation;

adapted "obtain" proofs;

provide case names for rev_induct, rev_cases;

rev_exhaust: rulify;

removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);

"atomize" for classical tactics;

atomize: all automated tactics that "solve" goals;

fixed two obscurities of "fix": predeclare_terms;

tuned names;

improved handling of "that": insert into goal, only declare as Pure "intro"; eliminated functor;

assumption / finish: handle non-atomic assumptions from context as well;

added atomic_judgment;

structure Obtain = Obtain;

new lemma card_Diff2_less for mulilated chess board

*** empty log message ***

*** empty log message ***

*** empty log message ***

the section command will belong to the new file

advanced induction examples

auto update?

replaced Acc.thy by Advanced.thy

no longer needed: too complicated an example

*** empty log message ***

auto generated

tuned goal output;

*** empty log message ***

*** empty log message ***

updated;

tuned goals output;

improved statement bindings for props; tuned;

converse: syntax \<inverse>;

tuned;

added ex/PER.thy;

improved doc of "subgoals" antiquotation;

replaced \isasymmacron by \isasyminverse;

tuned tex template;

Partial equivalence relations (leftover from HOL/Quot);

added antiq. subgoals

Added antiquotation "subgoals".

Mod because of additional parameters to pretty_goals.

back to 1.167, due to Emacs/CVS casualty!!;

added instantiate_tac

*** empty log message ***

removed isabelle resources: are available from main pages

cleanup, looks ok now with konqueror, too

*** empty log message ***

*** empty log message ***

added the $Id:$ line

*** empty log message ***

*** empty log message ***

use Library/List_Prefix;

added HOL/Library/List_Prefix;

improved antiquotations;

added \isarantiq;

add \<le> to list of "good" symbols;

tuned names;

added List_Prefix;

more "xsymbols" syntax;

"List prefixes" library theory (replaces old Lex/Prefix);