Minor tidying up.

Removal of leading "\!\!..." from most Goal commands

new stac

CHANGED_GOAL added to declare a more robust stac

inj_on

stac now uses CHANGED_GOAL and correctly fails when it has no useful effect, even for conditional rewrites

Corrected dead link.

Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default

massive tidying of proofs

renamed mutex to Acts

Replace awkward primrec by recdef.

swapped condition in update_apply.

isatool expandshort;

the distribution now includes Isabelle icons: see lib/logo/isabelle-{small,tiny}.xpm;

added xpm icons;

Converted to Auto_tac

several new basic modules made available for general use;

cleaned up;

theory Main includes everything;

reorganized the main HOL image;

stepping stones: Recdef, Main; String now part of main HOL;

stepping stones;

removed duplicate thms;

moved String theory to main HOL;

Removed disjE from list of rules used to simplify elimination rules because it made mk_cases fail if elimination rules contained disjunctive side conditions.

Removed leading !! in goals

Removed leading !! in goals.

Removed leading !! in goals.

Renamed expand_if to split_if and setloop split_tac to addsplits, as in HOL

HACKED declaration of addsplits

Deleted leading parameters thanks to new Goal command

tuned comment;

Symbol.beginning;

Uncurried functions LeadsTo and reach Deleted leading parameters thanks to new Goal command

fixed Integ;

Adapted to new inductive definition package.

Fixed bug (improper handling of flag no_ind).

Replaced "use_dir" command by "use", because nested calls of "use_dir" cause the HTML generator to crash.

HOL-Real

tuned Inductive.thy;

added add_typedecls;

Removed structure Prod_Syntax.

Adapted to new inductive definition package.

Adapted to new inductive package.

Removed obsolete comments.

Removed old inductive definition package.

Removed structure Prod_Syntax.

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;

isatool fixgoal;

Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb. The former format was just a hack to invoke type distinctions, while the latter uses the explictness principle.

comments and minor tidying

simplified and tidied the proofs

check_mlhome_file;

isatool fixgoal;

isatool fixgoal;

def_sort;

renamed Thm(s) back to thm(s);

export mk_triple1/2;

added read_def_axm;

added fix_mixfix;

fixed comment

tidying

New example Kerberos_BAN by G Bella

fixed comment;

tuned \s pattern;

isatool fixgoal;

removed Thy; the_context made public;

replaced warning by error_msg;

new toplevel commands `Goal' and `Goalw'; isatool fixgoal;

renamed thm(s) to Thm(s);

replace goal(w) commands by implicit versions Goal(w);

Goal and Goalw

goal -> Goal

Changed and changed back.

Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.

added General/history.ML;

Histories of values, with undo and redo;

use_text replaces use_strings;

handle_error: capture error msgs, even if no exception raised;

removed use_text;

added use_text;

Context.add_session;

changed (| |) syntax to (: :);

changed {: :} syntax to (| |);

tuned exports; added Thy;

removed rel.ML

ancient relic

Context.the_context;

get_context renamed to the_context; added get_context, set_context;

tuned transaction;

tuned comments;