Adapted to new inductive definition package.

Moved most of the Prod_Syntax - stuff to HOLogic.

Added additional theorems needed for inductive definitions.

New inductive definition package

added quick_and_dirty flag;

moved actual (C)Pure theories to pure.ML;

tuned transaction; moved actual (C)Pure theories to pure.ML;

use_text: verbose flag;

New rewrite unit_abs_eta_conv to compensate for unit_eq_proc

New rewrite unit_abs_eta_conv to compensate for unit_eq_proc

fixed unit_eq;

delsimprocs [unit_eq_proc];

simplification procedure unit_eq_proc rewrites (?x::unit) = (); quote / antiquote translations;

tuned loose bound vars check; added quote_antiquote_tr(');

added unit_eq simplification procedure;

added XX_YY_rewrite: simpset -> cterm -> thm;

Thm.rewrite_cterm;

defaults for free variables hide consts of same name;

added rewrite_cterm;

Installation of target HOL-Real

* HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...].

Ran isatool fixgoal

removed duplicate entry for Goal

Trivial change to be more like paper

Tidying; renaming of Says_Server_message_form to Says_Server_not_range; removal of junk from analz_spies_tac; removal of B~:bad premise from no_nonce_YM1_YM2

*** empty log message ***

Consequences of the change from [ := ] to ( := ) in theory Update.

Replaced [ := ] syntax by ( := ). Also allows ( := , := , ...) now.

isatool fixgoal;

isatool fixgoal;