fixed document;

added HOL/ex/Hebrew.thy; tuned;

obsolete;

command 'thms_containing' has been discontinued in favour of 'find_theorems'; TableFun/Symtab: curried lookup and update; tuned;

Revert previous attribute name change, problem can be avoided in JAXB.

forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;

extend: NameSpace.default_naming;

the experimental tagging system, and the usual tidying

Change PGIP attribute name class->messageclass to avoid Java keyword clash.

AList, the_*

fixed type annotation

added gen_list to Pretty module

@{term [source] ...} in subsections probably more robust;

tuned;

hide: added option '(open)';

imports Commutative_Ring instead of Main, since the latter hides our names;

hide the rather generic names used in theory Commutative_Ring;

renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;

... prem19

added prem10 - prem19

removed syntax fun_map_comp; introduced map_comp;

Unfortunately patched to use IntInf.int instead of just int (SML compatibility)

Method comm_ring for proving equalities in commutative rings.

tuned headers etc.;

fixed some ML names;

imports Commutative_Ring;

HOL: method comm_ring; Proof General: Unicode (UTF-8) support;

tuned;

no longer prefer xemacs, which fails more often than GNU emacs;

Bernhard Haeupler: comm_ring;