New datatype definition package

induct_tac -> exhaust_tac in 2 places.

moved long_names / cond_extern to name_space.ML;

tuned;

tuned;

fixed eps/ps find;

fixed CVSROOT;

fixed isabelle logo;

library includes Isabelle version information;

isatool expandshort;

fixed isabelle logo;

SYNC;

added pdfsetup and isabelle logo;

SYNC;

Added acc_downwards

Added simproc list_eq.

Simplified last proof.

ZF: Main, Update

added case_tac to be like HOL

added Main and Update

as in HOL

A stronger apply_0, and new thm domain_lam

added comments

tidying

now with Goal cmd

tidying

Got rid of obsolete "goal" commands. Also inserted spaces after all periods

Addition of "Theorem B" of Peter Andrews

Fixed bug in transform_rule.

More tidying and removal of "\!\!... from Goal commands

More tidying and removal of "\!\!... from Goal commands

@ -> $

disjoint

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;

adapted to TheoryDataFun interface;

moved attributes theory data to Isar/isar_thy.ML;

moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;

added exnMessage;

added General;

added of_file;

General tools.

moved table.ML, object.ML, seq.ML, name_space.ML to General;

moved object.ML to General/object.ML;

moved table.ML to General/table.ML;

moved seq.ML to General/seq.ML;

moved position.ML, path.ML, file.ML to General;

moved name_space.ML to General/name_space.ML;

moved Thy/path.ML to General/path.ML;

moved Thy/position.ML to General/position.ML;

moved Thy/file.ML to General/file.ML;

new type-safe user interface for theory data;

nonterminals prog;

adapted to new theory data interface;

use type-safe theory data interface;

added theory_data.ML;

Type-safe interface for theory data.

* improved the theory data mechanism to support real encapsulation; main change of the internal interfaces: data kind name (string) replaced by private Object.kind, acting as authorization key;

accomodate tuned version of theory data;

added print_theorems: theory -> unit; added print_theory: theory -> unit; added transaction mechanism as last resort to accomodate non-atomic transformers (please avoid such things); tuned setup;

Object.T;

improved data: secure version using Object.T and Object.kind;

tuned setup; tuned add_attributes: comment; accomodate tuned version of data;

use Object.T and Object.kind; added print_data; improved get_data, put_data: more abstract; add_axioms(_i), add_oracle: made atomic transactions;

removed type object (see object.ML);

tuned print_exn;

print_data moved to theory.ML; print_theory: exclude theorems (no forward reference!);

added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; added ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added EVERY: ('a -> 'a seq) list -> 'a -> 'a seq; added FIRST: ('a -> 'b seq) list -> 'a -> 'b seq; added TRY: ('a -> 'a seq) -> 'a -> 'a seq; added REPEAT: ('a -> 'a seq) -> 'a -> 'a seq;

added object.ML;

added option_map_o_empty added option_map_o_empty and option_map_o_update to simpset()

added split_etas

added split_sum_case_asm

tuned;

tuned msgs;

auto update

fixed ml_prompts;

changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option;

tuned dist version;

tuned header;

version under control of Admin/makedist;

README, Pure/ROOT.ML: version set automatically;

version under control of Admin/makedist; ml_prompts;

added ml_prompts;

added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source; (map)filter: fixed propagation of prompt;

tuned error msg;

fixed error msgs;

Structure Option now declared in MLWorks

mk_all_imp: no longer creates goals that have beta-redexes

more tracing

Changed require to requires for MLWorks

auto update

made SML/NJ happy;

foldl_map prep_field;

tuned store_theory;

tuned local, global; tuned begin and end theory;

tuned store_theory: theory -> unit;

added get_name, put_name, global_path, local_path, begin_theory, end_theory;

global_names moved to pure_thy.ML;

certify_term: type_check replaces Term.type_of, providing sensible error messages; eliminated mapfilt_atoms (use Term.foldl_aterms);

renamed state_source to source'; removed test;

added recover, source;

added catch: ('a -> 'b) -> 'a -> 'b; tuned source(');

remove seq2, scan (use seq2, foldl_map from library.ML);

added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit; tuned 'beginning';

Swapped order of params.

changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source; tuned prompt; Scan.source vs. Scan.source';

source vs. source';

tuned keywords;

added is_stale;

tuned signature; added pretty_theory;

tuned comments;

tuned;

Small mods.

prompt made part of source;

fixed handle_error: cat_lines;

added Thy/position.ML;

added source: string -> (string, string list) Source.source;

Input positions.

added Syntax/source.ML;

added Source module;

Co-algebraic data sources.

Symbol.stopper;