2005-09-15 wenzelm [Thu, 15 Sep 2005 17:17:02 +0200] rev 17414
The Hebrew Alef-Bet -- Unicode example;
src/HOL/ex/Hebrew.thy

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:17:01 +0200] rev 17413
added Hebrew.thy;
src/HOL/ex/ROOT.ML

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:16:56 +0200] rev 17412
TableFun/Symtab: curried lookup and update;
TFL/casesplit.ML TFL/thry.ML src/HOL/Import/hol4rews.ML src/HOL/Import/proof_kernel.ML src/HOL/Matrix/cplex/CplexMatrixConverter.ML src/HOL/Matrix/cplex/Cplex_tools.ML src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML src/HOL/Matrix/cplex/fspmlp.ML src/HOL/Tools/ATP/res_clasimpset.ML src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_aux.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/record_package.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/res_clause.ML src/HOL/Tools/typedef_package.ML src/Provers/Arith/cancel_numerals.ML src/Provers/Arith/combine_numerals.ML src/Provers/Arith/extract_common_term.ML src/Pure/General/graph.ML src/Pure/General/name_space.ML src/Pure/General/output.ML src/Pure/General/symbol.ML src/Pure/General/table.ML src/Pure/IsaPlanner/term_lib.ML src/Pure/Isar/attrib.ML src/Pure/Isar/isar_output.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/term_style.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/Proof/proofchecker.ML src/Pure/Proof/reconstruct.ML src/Pure/Syntax/ast.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syntax.ML src/Pure/Thy/html.ML src/Pure/Thy/present.ML ...

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:16:55 +0200] rev 17411
fixed document;
src/HOL/Auth/OtwayRees.thy src/HOL/Auth/Yahalom.thy

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:16:54 +0200] rev 17410
added HOL/ex/Hebrew.thy;
tuned;
src/HOL/IsaMakefile

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:16:53 +0200] rev 17409
obsolete;
Admin/BUGS

2005-09-15 wenzelm [Thu, 15 Sep 2005 17:16:53 +0200] rev 17408
command 'thms_containing' has been discontinued in favour of 'find_theorems';
TableFun/Symtab: curried lookup and update;
tuned;
NEWS

2005-09-15 aspinall [Thu, 15 Sep 2005 16:15:22 +0200] rev 17407
Revert previous attribute name change, problem can be avoided in JAXB.
src/Pure/proof_general.ML

2005-09-15 wenzelm [Thu, 15 Sep 2005 13:36:10 +0200] rev 17406
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
src/Pure/Isar/isar_thy.ML

2005-09-15 wenzelm [Thu, 15 Sep 2005 13:35:21 +0200] rev 17405
extend: NameSpace.default_naming;
src/Pure/sign.ML