2006-04-08 wenzelm [Sat, 08 Apr 2006 22:51:06 +0200] rev 19363
refined 'abbreviation';
NEWS doc-src/IsarRef/generic.tex src/FOL/IFOL.thy src/HOL/Auth/Guard/Guard_Shared.thy src/HOL/Equiv_Relations.thy src/HOL/Finite_Set.thy src/HOL/Fun.thy src/HOL/Infinite_Set.thy src/HOL/Isar_examples/Hoare.thy src/HOL/Lambda/Commutation.thy src/HOL/Lambda/Eta.thy src/HOL/Lambda/Lambda.thy src/HOL/Lambda/ListApplication.thy src/HOL/Lambda/ListBeta.thy src/HOL/Lambda/ParRed.thy src/HOL/Lambda/Type.thy src/HOL/Lambda/WeakNorm.thy src/HOL/Library/Accessible_Part.thy src/HOL/Library/Multiset.thy src/HOL/List.thy src/HOL/Relation.thy src/HOL/Set.thy src/HOL/Unix/Unix.thy src/HOL/ex/Abstract_NAT.thy src/HOL/ex/Classpackage.thy

2006-04-08 haftmann [Sat, 08 Apr 2006 22:12:02 +0200] rev 19362
made symlink relative
Admin/website/build/project.mak

2006-04-08 haftmann [Sat, 08 Apr 2006 22:10:58 +0200] rev 19361
made symlink relative
Admin/website/build/project.mak

2006-04-08 kleing [Sat, 08 Apr 2006 15:24:21 +0200] rev 19360
converted Müller to Mueller to make smlnj 110.58 work
src/HOLCF/IOA/ABP/Check.ML src/HOLCF/IOA/ABP/Correctness.ML src/HOLCF/IOA/ABP/Lemmas.ML src/HOLCF/IOA/ABP/ROOT.ML src/HOLCF/IOA/Modelcheck/ROOT.ML src/HOLCF/IOA/NTP/Abschannel.ML src/HOLCF/IOA/NTP/ROOT.ML src/HOLCF/IOA/ROOT.ML src/HOLCF/IOA/Storage/Correctness.ML src/HOLCF/IOA/Storage/ROOT.ML src/HOLCF/IOA/ex/ROOT.ML src/HOLCF/IOA/ex/TrivEx.ML src/HOLCF/IOA/ex/TrivEx2.ML src/HOLCF/IOA/meta_theory/Abstraction.ML src/HOLCF/IOA/meta_theory/Asig.ML src/HOLCF/IOA/meta_theory/CompoExecs.ML src/HOLCF/IOA/meta_theory/CompoScheds.ML src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/IOA/meta_theory/Compositionality.ML src/HOLCF/IOA/meta_theory/Deadlock.ML src/HOLCF/IOA/meta_theory/LiveIOA.ML src/HOLCF/IOA/meta_theory/RefCorrectness.ML src/HOLCF/IOA/meta_theory/RefMappings.ML src/HOLCF/IOA/meta_theory/ShortExecutions.ML src/HOLCF/IOA/meta_theory/SimCorrectness.ML src/HOLCF/IOA/meta_theory/Simulations.ML src/HOLCF/IOA/meta_theory/TL.ML src/HOLCF/IOA/meta_theory/TLS.ML src/HOLCF/IOA/meta_theory/Traces.ML

2006-04-07 berghofe [Fri, 07 Apr 2006 17:27:53 +0200] rev 19359
Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".
src/HOL/Tools/inductive_package.ML

2006-04-07 kleing [Fri, 07 Apr 2006 12:48:10 +0200] rev 19358
remame ASeries to Arithmetic_Series
src/HOL/Complex/ex/ASeries_Complex.thy src/HOL/Complex/ex/Arithmetic_Series_Complex.thy src/HOL/Complex/ex/ROOT.ML

2006-04-07 berghofe [Fri, 07 Apr 2006 11:17:44 +0200] rev 19357
Added alternative version of thms_of_proof that does not recursively
descend into proofs of (named) theorems.
src/Pure/proofterm.ML

2006-04-07 mengj [Fri, 07 Apr 2006 05:14:54 +0200] rev 19356
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
src/HOL/Tools/ATP/res_clasimpset.ML

2006-04-07 mengj [Fri, 07 Apr 2006 05:14:06 +0200] rev 19355
filter now accepts axioms as thm, instead of term.
src/HOL/Tools/ATP/reduce_axiomsN.ML

2006-04-07 mengj [Fri, 07 Apr 2006 05:12:51 +0200] rev 19354
tptp_write_file accepts axioms as thm.
src/HOL/Tools/res_clause.ML src/HOL/Tools/res_hol_clause.ML