adapted to inner syntax of sorts;

replaced {{ }} by { };

added sort_of_term; export sortT;

added read_sort;

*** empty log message ***

new stuff;

\urlstyle{rm};

snapshot of new Isar'ized version;

added lemma.

fixed link

* HOL/ML: even fewer consts are declared as global (see theories Ord, Lfp, Gfp, WF); this only affects ML packages that refer to const names internally; * 'pr' command: no longer prints theory contexts, but only proof states;

print_state: flag for proof only;

hide: check declared;

added disable_pr, enable_pr;

'pr' now prints actual proof states only;

fewer consts declared as global;

'apply' consumes facts;

Proof General -- if present make this the default;

export generic_simp_tac;

changed to cope with the rewriting of #2+n to Suc(Suc n)

new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2

reverted to old proof of dominoes_tile_row, given new treatment of #2+...

Replaced some definitions involving epsilon by more readable primrec definitions.

alist_rec and assoc are now defined using primrec and thus no longer refer to the recursion combinator list_rec, which should be considered internal.

Removed unnecessary primrec equations of hd and last involving arbitrary.

collected three proofs into rename_client_map_tac

added the dummy theory Integ/NatSimprocs.thy

updated