HOL/IMP: include session graph;

updated;

tuned;

removed preallocated heaps axiom (now in type safety invariant)

updated;

New type definition diagram

added exec_lub

new type definition figure

minor suggestions from Markus

additional material

* system: tested support for MacOS X;

better simplification makes steps redundant

replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll by lesspoll_trans1, lesspoll_trans2

tuned;

use Locale.read/cert_context_statement;

*** empty log message ***

tuned;

improved mixfix_args;

tuned Type.unify; do *not* declare TVar names as used;

simultaneous type-inference of complete context/statement specifications; reorganized code;

tuned interface of unify, param; added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;

tuned Type.unify;

mods due to changed 1-point simprocs (quantifier1).

mods due to improved 1-point simprocs (quantifier1).

mods due to mor powerful simprocs for 1-point rules (quantifier1).

now permutations of quantifiers are allowed as well.

fixed JVMListExample

MicroJava exception merge

temporarily removed JVMListExample

exception merge + cleanup

exception merge, doesn't work yet

exception merge, cleanup, tuned

exceptions

list_all2_rev

removed debug stuff;

support for ``indexed syntax'' (using "\<index>" argument instead of "_");

removed special treatment of "_" in syntax (now covered by \<index> arg);

tuned locale interface;

proper treatment of internal parameters;

\usepackage[latin1]{inputenc};

Wenzel:2001:Isar-examples;

updated;

mixfix syntax for selectors;

record: mixfix;

export used_types; tuned;

Locale.activate_context;

beginning support for type instantiation; tuned internal arrangements;

varify returns newly introduced variables;

varifyT' returns newly introduces variables;

added invent_type_names; added add_tvarsT etc. (from drule.ML);

changed Thm.varifyT';

type_env;

added type_env function; let norm_type_XXX work directly with type env component;

export add_tvarsT etc.;

changed Type.varify;

Term.invent_type_names;

*** empty log message ***

*** empty log message ***

made SML/XL happy;

*** empty log message ***

Terminator now uses arith_tac as well.

comp -> rel_comp

isatool expandshort;

Relaxed the precondition of UN_upper_le

isatool expandshort;

new rewrite rules for use by arith_tac to take care of uminus. mods due to reorienting and renaming of real_minus_mult_eq1/2

new rewrite rules for use by arith_tac to take care of uminus.

mods due to reorienting and renaming of real_minus_mult_eq1/2

tuned conversion from terms to "polynomials" for arith_tac: takes care of "uminus" now.

drop_judgment: be graceful about undeclared judgment;

obsolete;

option "-d pdf" by default (accomodates pdf bias of Mac OS X); tuned getpwnam;

removed installfonts, xterm interface; improved default of PROOFGENERAL_OPTIONS;

Removed pointless backtracking from arith_tac

Improved error messages.

*** empty log message ***

tuned;

obsolete;

obsolete;

tuned;

\isasymindex made text mode;

isatools "symbolinput" and "nonascii" have disappeared;

added HOL-Library;

tuned;

updated;

removed altogether;

removed unused stuff;

Updated.

oops;

bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";

updated reserved words of HOL;

* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;

obsolete;

removed additional blank line (confuses some versions of make);

obsolete;

- Changed type of invoke_codegen - Added combinators for sequences

- Added code generator interface for types - Changed type of invoke_codegen

Fixed bug in function find_paths.

Added example file for intuitionistic logic (taken from FOL).

Added support for code generation.

Recursive equations to be used for code generation are now registered via RecfunCodegen.add

Code generator for recursive functions.

Tuned header.

Code generator for datatypes.

Moved contents to files datatype_codegen.ML and recfun_codegen.ML

Turned subcls1 into an inductive relation to make it executable.

Example for code generator.

Added examples for code generator.

Added code generator setup.

Tuned code generator setup.

Added new files (code generator and examples).

Moved code generator setup from Recdef to Inductive.

Replaced several occurrences of "blast" by "rules".

document root;

tuned

HOLCF/IMP converted to Isar

HOL/IMP converted to Isar

converted to Isar

latex output setup

tuned for latex output

setup [trans] rules for calculational Isar reasoning

use /var/tmp (which happens to be more spacious on atbroy37);

new-style theory; proper declarations of various induction rules;

added Main.ML;

restart_loader: do *not* ThyLoad.reset_path;

tuned print_state interfaces;

optional PGML markup;

added writelns;

use "xml.ML";

export writeln_default; tuned prefix_lines;

tuned print_goals interfaces;

added General/xml.ML;

Basic support for XML output.

Slightly generalized the agents' knowledge theorems

added default_type;

tuned line breaks in HTML source;

fixed dest atts;

refrain from peeking at tags;

include session graph;

replaced record_split by the cases method

intro and elim now require arguments

record extend and truncate exercises

use Main;

* Pure/obtain: "thesis" now internal (use ?thesis); * Pure: generic 'sym' / 'symmetric' attributes; * Provers/classical: 'swapped' attribute; * HOL: proper rules less_induct and wf_induct_rule;

Syntax.internal thesis;

tuned xtra_netpair;

clarified sym_del;

added 'swapped' attribute; tuned xtra_netpair; tuned;

added the_mk_cases;

tuned;

renamed Finite to Finite_Set;

less_induct, wf_induct_rule;

renamed theory Finite to Finite_Set and converted;

this material already part of HOL/Set.thy;

sym [sym];

tuned;

iff;

updated;

adapted intr/elim uses;

eliminated old use of intro/elim method; tuned;

simplified proof (no longer use swapped rules);

fixed intro steps;

tuned declarations (rules, sym, etc.);

removed unused functionality (weight etc.);

simple version of 'intro' and 'elim' method; use ContextRules.find_rules;

added 'print_rules' command;

added print_rules;

simplified NetRules;

export low-level addXXs; find_rules interface;

added 'sym' and 'symmetric' atts;

removed bang_args;

'symmetric' attribute moved to Pure/calculation.ML;

simplified (and clarified) integration with Pure/ContextRules; removed "extra" rules as separate slots, only keep xtra_netpair for single-step view of plain haz/safe rules;

iff?: refer to Pure/ContextRules;

ContextRules.intro_bang_global;

added add_rule, del_rule;

tuned declarations;

tuned;

added ex/First_Order_Logic.thy, ex/document/root.tex;

added First_Order_Logic.thy;

sym declarations; tuned declarations;

removed declaration of disjI1, disjI2 (already done in IFOL);

removed AddXIs, AddXEs, AddXDs;

updated;

* Pure/Provers/classical: simplified integration with pure rule attributes and methods;

reactivate tracing markup;

made SML/NJ happy;

made slightly more robust;

added Higher_Order_Logic.thy;

rules_tac: SELECT_GOAL!!; tuned;

disable markup of tracing output (tmp?);

\usepackage{textcomp};

removed \newcommand{\isasymone};

hyp_subst_tac';

setup "rules" method;

no need for hyp_subst_tac' (!?);

renamed RuleContext to ContextRules;

\usepackage{textcomp}, \usepackage{marvosym};

renamed rule_context.ML to context_rules.ML;

setup "rules" method;

interface for wrappers;

added "rules" method;

removed questionable init_gensym;

hyp_subst_tac';

use \<zero>, \<one>;

\renewcommand{\isasymzero}, \renewcommand{\isasymone};

updated;

HOLogic.read_cterm;

HOLogic.typeS;

removed dead code;

renamed class "term" to "type" (actually "HOL.type");

added zero--nine, euro; tuned some text symbols;

%\usepackage{textcomp} %\usepackage{marvosym}

* HOL: the class of all HOL types is now called "type" rather than "term"; INCOMPATIBILITY, need to adapt references to this type class in axclass/classes, instance/arities, and (usually rare) occurrences in typings (of consts etc.); internally the class is called "HOL.type", ML programs should refer to HOLogic.typeS;

*** empty log message ***

minor tweaks

*** empty log message ***

*** empty log message ***

*** empty log message ***

minor textual tweaks

*** empty log message ***

*** empty log message ***

export primitive netpairs; activate attributes;

RuleContext.intro_query_local;

rule context and attributes moved to rule_context.ML;

qualify_elem: do not qualify empty names ("");

tuned;

added deletion of rules; tuned;

general type of delete_tagged_brl; tuned;

most general type of delete/delete_term;

skip_proof: do not require quick_and_dirty in interactive mode;

support "_::foo" sort constraints;

removed unused simple_read_typ; read_typ, TypeExt.typ_of_term: map_sort argument;

added proof_to_theory';

Syntax.typ_of_term: pass intern sort fn;

Syntax.read_typ: pass intern sort fn;

* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; * Pure/syntax: "x::_::foo" sort constraints;

theory data: removed obsolete finish method;

data: removed obsolete finish method;

name space for local thms (export cond_extern, qualified); improved internal naming of fixes;

print_state: up to 7 result names;

qualify imported facts; clarified read/cert_element; theory data: removed obsolete finish; tuned;

variant: preserve suffix of underscores (for skolem/internal names etc.);

join_rules RuleCases.save;

tuned declarations;

tuned;

make SML/NJ happy;

added Pure/Isar/rule_context.ML;

gcd_dvd1 and gcd_dvd2 proven simultaneously;

moved lemmas to theory Hilbert_Choice;

tuned; meson lemmas from Tools/meson.ML;

added remdups_rl;

clarified order of merge_lists';

clarified order in gen_merge_lists';

fixed SML/NJ error (!?);

use merge_lists, merge_alists;

Symtab.merge_multi'; tuned;

type variables: clarified "used" vs. "occ";

Library.gen_merge_lists';

clarified locale operations (rename, merge); tuned;

print_locale: expr;

added join, merge_multi('); tuned extend, make, merge;

merge_stamps: merge_lists' with reversed args;

gen_merge_lists;

added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;

gen_merge_lists';

generic_merge;

converted simp lemmas;

tuned;

Extended match_proof to handle abstractions.

tuned;

improved ordering of evaluated elements;

time_use_thy "Locales";

Isar conversion

theory Locales temporarily disabled;

beginnings of actual locale expressions;

improved locale expression syntax;

locale expression import;

import locale expression;

tuned;

added uname; syntax for locale expressions (presently unused);

tuned;

thm "point.defs";

recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";

renamed "fields" to "flds" (avoid clash with new "fields" operation);

locale expressions;

use tracing function for trace output;

tracing_fn;

added tracing, tracing_fn;

Set.vimage;

got rid of theory Inverse_Image;

theory Inverse_Image converted and moved to Set;

tuned;

tuned;

fixed links etc.;

* HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;

prefer later trfuns;

moved prefixes1, suffixes1 to library.ML;

trfuns *after* binder syntax;

added prefixes1, suffixes1;

print_depth 10;

derive cases/induct rules for ``more'' parts;

tuned;

Hyperreal

improved treatment of common result name;

tuned;

multi_theorem: common statement header (covers *all* results);

fixed comment; goal: unbind if multiple statements;

induct method: localize rews for rule;

Now handles different theorems with same name more gracefully.

Improved error message.

Added setup.

Moved fastype to Envir.

Further restructuring of theorem naming functions.

Added setup for proof rewrite rules.

- Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data

Replaced devar by Envir.head_norm

Moved head_norm and fastype from unify.ML to envir.ML

fixed maxs bug

Ntree and Brouwer converted and moved to ZF/Induct;

converted;

actually store "coinduct" rule;

additional P.marg_comment;

\usepackage[latin1]{inputenc};

even more theories from Jacques

finish_global: Drule.strip_shyps_warning (just for warning);

ext_tsig_classes: rebuild_tsig!!!!!

local_standard: plain strip_shyps instead of strip_shyps_warning;

last-minute tidying

updated;

GPLed;

write_keywords: string argument (logic name);

isatool unsymbolize;

Modified to make the files build with the new changes in ZF

depends on Epsilon!

fix_frees: rev;

prove: raise ERROR_MESSAGE;

updated;

* ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);

setup DatatypeTactics.setup;

added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);

no handle ERROR;

fixed;

Isar version of 'rep_datatype';

avoid handle _;

added TCSET(') tacticals;

added Term and Tree_Forest (from converted ZF/ex);

TF and Term moved to ZF/Induct;

miniscoping of UN and INT

Added new entry

New files

new theories from Jacques Fleuriot

*** empty log message ***

converted datatype examples moved from ZF/ex to ZF/Induct;

document setup;

removed BT, Data, Enum (see ZF/Induct);

case_names;

added Datatypes, Binary_Trees (from ZF/ex);

Isar attribute and method setup;

fix path prefix;

use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;

added Induct/Binary_Trees.thy, Induct/Datatypes.thy; removed ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy;

tuned;

updated;

adapted primrec/datatype to Isar;

tuned;

store original simps for codegen;

inductive: removed con_defs;

updated;

updated;

* ZF: new-style theory commands 'inductive', 'inductive_cases', and methods 'ind_cases', 'induct_tac', 'case_tac';

ZF specific keywords;

rearranged inductive package for Isar;

Generic inductive cases facility for (co)inductive definitions.

converted;

tuned;

tuned inductions;

prove: Envir.beta_norm;

new SList theory from Bu Wolff

induct: rule_versions produces localized variants;

empty rule_context for multiple goals;

added empty;

mutual rules declared as ``consumes 0'';

induct_atomize: include atomize_conj (for mutual induction);

Isar: 'induct' proper support for mutual induction involving non-atomic rule statements; Isar/Pure: support multiple simultaneous goal statements;

proper handling of mutual rules (esp. for sets);

lemmas induct_atomize = atomize_conj ...; val local_imp_def = thm "induct_implies_def";

val local_imp_def = thm "induct_implies_def";

ZF/Induct,UNITY

Tidying necessitated by new simprules in equalities.ML

conditional miniscoping equalities now made unconditional

new-style numerals without leading #, along with generic 0 and 1

congc now returns None if congruence rule has no effect.

Renamed some bound variables due to changes in simplifier.

Fixed proof depending on strange behaviour of rename_bvs.

Renamed some bound variables due to changes in simplifier.

present multi_result;

added meta_conjunction_tr';

pure_syntax_output: "_meta_conjunction";

adapted to multiple results;

adapted auto_bind_goal, auto_bind_facts;

added multi_theorem(_i); have, show etc.: multiple statements;

Proof.have_i: multiple statements;

added RAW_METHOD, RAW_METHOD_CASES; METHOD, METHOD_CASES etc.: conjunction_tac;

added add_thmss;

"theorem" etc.: multiple statements;

theorem, have, show etc: multiple statements;

facts: multiple args;

added conjunction_tac;

renamed open_smart_store_thms to smart_store_thms_open; added Syntax.pure_syntax_output;

added mk_conjunction;

added unflat;

added conj_elim_precise, conj_intr_thm;

use Tactic.prove;

tuned;

support co/inductive definitions in new-style theories;

adapted to add_inductive_x;

syntactic declaration of external *and* internal versions of fixes; tuned warn_extra_tfrees;

fixed print_records;

tuned;

theorems case_split = case_split_thm [case_names True False, cases type: o];

Theorems symmetric, reflexive and transitive are now stored with "open" derivations.

Commands prf and full_prf can now also be used to display proof term of current proof state.

eliminated old "symbols" syntax, use "xsymbols" instead;

theory data: finish method;

indexvar_ast_tr (for \<index> placeholder);

removed pure_sym_syntax; allow additional arguments in infixes (maximum priority);

File.use;

added impose_hyps_tac; robustify insts of tactic emulations;

proper close_locale;

no longer support "isabelle_font" or "symbols";

got rid of obsolete input filtering;

back to normal; tuned;

eliminated old "symbols" syntax, use "xsymbols" instead;

updated;

got rid of obsolete input filtering and isabelle font encoding;

got rid of obsolete input filtering;

eliminated old "symbols" syntax, use "xsymbols" instead;

theory data: finish method;

removed needs_filtered_use;

\newcommand{\isasymindex}{\isamath{\i}};

* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.) now consider the syntactic context of assumptions, giving a better chance to get type-inference of the arguments right (this is especially important for locales); * system: refrain from any attempt at filtering input streams; no longer support ``8bit'' encoding of old isabelle font, instead proper iso-latin characters may now be used;

tuned;

\bibliographystyle{abbrv};

updated;

make SML/XL of NJ happy;

ex/document/root.bib;

proper syntax for structs;

more explanations on advanced syntax;

use num_const of Pure;

\newcommand{\isasymstruct}{\isamath{\diamond}};

locale_prefix: Sign.base_name;

syntax for structs;

tuned;

syntax for structures;

tuned impose_hyps;

added structures; tuned;

\isasymstruct;

Sidi Ehmety's port of the fold_set operator and multisets to ZF. Also, fixes to the cancellation simprocs and a few new standard lemmas.

reorganization of the ZF examples

tuned;

cert_def: proper check of args, improved msgs; tuned;

pretty_goals_local: observes context syntax; PureThy.store_thm: locale_prefix;

defines: Thm.def_name, proper check of args;

separate "in" locale vs. ad-hoc context;

goals_limit moved to display.ML;

added goals_limit (from tctical.ML); added pretty_goals_aux, removed excessive variants of print_goals;

use_thy "Locales";

use locales instead of consts/axioms;

* Isar/Pure: proper integration with ``locales''; unlike the original version by Florian Kammueller, Isar locales package high-level proof contexts rather than raw logical ones (e.g. we admit to include attributes everywhere); * Isar/Pure: theory goals now support ad-hoc contexts, which are discharged in the result, as in ``lemma (assumes A and B) K: A .''; syntax coincides with that of a locale body;

activate dead code, make document work;

renamed Sqrt_Irrational.thy to Sqrt.thy;

Locales and simple mathematical structures;

renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy; added ex/Locales.thy;

extend_XXX: sane argument order ... -> syntax -> syntax;

local syntax: add_syntax, proper read/pretty functions;

locale_element/uses: string;

proper treatment of local syntax; store_thm: test atts; Uses: string;

print_syntax: include local version;

added pretty_term', read_typ', read_typ_no_norm', read_def_terms' which refer to local syntax;

export pretty_thm_aux;

tuned;

theorem(_i): locale atts; global_goal, finish_global: proper treatment of target locale;

group locale_element;

added add_locale(_i) and store_thm; removed old scope stuff; tuned;

theorem(_i): locale atts; added add_locale;

added 'locale', 'print_locales', 'print_locale';

added print_locales, print_locale;

added "locale", "print_locale", "print_locales";

fixes: optional typ; removed garbage;

added pretty/print functions with context; added cert_def; print_asms covers both fixes and assumes;

locale_element: optional typ;

pretty/print functions with context;

export add_tvarsT, add_tvars, add_vars, add_frees (would actually belong to term.ML, but is apt to cause some confusion with the fold-right versions there);

Method.trace ctxt;

tuned;

new Sqrt example

tuned comment;

simplified Proof.init_state:

added get_thms_with_closure; fix_frees: only new ones;

added locale_element;

locale elements;

theorem(_i): locale elements;

locale syntax;

IsarThy.theorem_i (None, []);

updated;

Fixed bug in function add_npvars.

updated;

tuned;

proper use of bind_thm(s);

adapted to new-style theories;

GPLed;

converted theory Dnat;

* 'domain' package adapted to new-style theories, e.g. see HOLCF/ex/Dnat.thy;

document setup;

replaced Undef by UU;

ax_flat;

GPLed;

tuned;

replaced Undef by UU;

converted theory Lift;

rep_datatype lift; converted to new-style theory;

moved into Main;

moved String into Main;

tuned;

HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac instead of lift.induct_tac, use UU instead of Undef in cases;

declare transitive;

theory Calculation move to Set;

transitive declared in Pure;

Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.

Goals.add_locale;

fix_frees; improved export_def: handle args on lhs;

theorem: locale argument;

beginnings of new locales (not yet functional);

Goals.setup;

parking code for old-style locales here;

tuned notation (degree instead of dollar);

theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");

Proof.init_state thy None;

simplified export; tuned printing of fixes;

'atomize': CHANGED_PROP;

global statements: locale argument;

added local_standard;

IsarThy.theorem_i: no locale;

removed obsolete (rule equal_intr_rule);

Additional rules for simplifying inside "Goal"

- Tuned add_cnstrt - Fixed bug in reconstruct_proof that caused infinite loop

Removed name_thm from finish_global.

Tuned function thm_proof.

- enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments

norm_hhf_eq is now stored using open_store_standard_thm.

induct: internalize ``missing'' consumes-facts from goal state (enables unstructured scripts to perform elim-style induction);

- 'induct' may now use elim-style induction rules without chaining facts, using ``missing'' premises from the goal state; this allows rules stemming from inductive sets to be applied in unstructured scripts, while still benefitting from proper handling of non-atomic statements; NB: major inductive premises need to be put first, all the rest of the goal is passed through the induction;

(induct set: ...);

put_consumes: really overwrite existing tag;

finish_global: Tactic.norm_hhf;

use HOL.induct_XXX;

use induct_rulify2;

renamed inductive_XXX to induct_XXX; added induct_impliesI;

induct_impliesI;

tuned induct proofs;

- 'induct' method now derives symbolic cases from the *rulified* rule (before it used to rulify cases stemming from the internal atomized version); this means that the context of a non-atomic statement becomes is included in the hypothesis, avoiding the slightly cumbersome show "PROP ?case" form;

tuned;

induct: cases are extracted from rulified rule;

removed obsolete make_raw;

lemma Least_mono moved from Typedef.thy to Set.thy;

tuned;

removed option -depend (not available everywhere?);

converted theory "Set";

fixed string_of_mixfix;

tuned declaration of rules;

equal_intr_rule already declared in Pure;

rules for meta-level conjunction;

tuned prove;

tuned;

added prove;

declare equal_intr_rule as intro;

tuned prove; added prove_standard;

removed obsolete goal_subclass, goal_arity;

use Tactic.prove;

use Tactic.prove; improved proof of equality rule;

tuned;

* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;

updated;

impose hyps on initial goal configuration (prevents res_inst_tac problems);

added "atomize" method;

prove: primitive goal interface for internal use;

added impose_hyps;

exclude field_simps from user-level "simps";

Isar: fixed rep_datatype args;

hardwire qualified const names;

removed "more" class;

moved product cases/induct to theory Datatype;

made new-style theory; tuned;

atomize_conj;

* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;

Fixed several bugs concerning arbitrarily branching datatypes.

Eliminated occurrence of rule_format.

tuned;

need at least 3 latex runs to get toc right!

tuned;

tuned;

Rrightarrow;

tuned notation;

tuned notation;

accomodate some recent changes of record package;

updated;

removed "more" sort; refer to properly named theorems internally;

updated records;

'simplified' att: args;

* HOL/record: - removed "more" class (simply use "term") -- INCOMPATIBILITY;

* Provers: 'simplified' attribute may refer to explicit rules instead of full simplifier context; 'iff' attribute handles conditional rules; * HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY; - new derived operations "make" (for adding fields of current record), "extend" to promote fixed record to record scheme, and "truncate" for the reverse; cf. theorems "derived_defs", which are *not* declared as simp by default; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;

Replaced main proof by proper Isar script.

derived operations are now: make, extend, truncate (cf. derived_defs);

tuned;

check_goal: setmp proofs 0;

added windowlistener (can now close the frame by window controls)

* HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - "record" operation truncates to particular fixed record (acts like a type cast); - make_defs no longer part of default simps; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;

innermost_params;

(simp add: point.make_def);

provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records;

further 1.73 changes: added fix_direct, simplified assume interface;

added read_prop_schematic;

simplified ProofContext.assume interface;

moved lambda to Pure/term.ML;

added lambda;

* clasimp: ``iff'' declarations now handle conditional rules as well;

added string_of_mixfix;

print_depth 8 from the very beginning;

added export_assume, export_presume, export_def (from proof.ML);

moved RANGE to tctical.ML; moved export_assume, export_presume, export_def to proof_context.ML;

added RANGE (from Isar/proof.ML);

print fixed names as plain strings;

eliminated old numerals;

use generic 1 instead of Numeral1; use improved iff declaration; tuned;

eliminated Numeral0;

build option enables most basic browser info (for proper recording of session);

build option;

tuned;

eliminated old numerals;

pass build mode to process;

removed export_thm;

trace_rules: only non-empty;

removed obsolete "exported" att;

replace_dummy_patterns: lift over bounds;

iff: always rotate prems;

apply(simp add: three_def numerals) (* FIXME !? *);

unset DISPLAY (again);

* Pure: removed obsolete 'exported' attribute; * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

*** empty log message ***

moved object_logic.ML to Isar/object_logic.ML;

moved locale.ML to Isar/locale.ML;

moved goal related stuff to goals.ML;

Display.current_goals_markers;

tuned;

moved prove_goalw_cterm to goals.ML; cleaned up;

moved local defs to proof.ML (for locales);

improved source arrangement of obtain;

rearrange sources for locales;

Display.print_current_goals_fn;

Display.print_goals;

Display.pretty_thms;

qualified names;

make this module appeat late in Pure; moved print_current_goals to display.ML; added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML); added thm database functions (from Thy/thm_database.ML);

print_goals stuff is back (from locale.ML);

reorganize sources to accomodate locales;

corollary;

quick_and_dirty_prove_goalw_cterm;

javac -depend;

-D generated;

Added "clean" target.

Fixed problem with batch mode layout, which caused an AWT exception when no X11 connection was available.

initBrowser now has additional noAWT argument.

Constructor no longer takes font as an argument.

Moved font settings from TreeNode to TreeBrowser.

Moved font settings from Vertex to GraphView.

deleted the redundant first argument of adjust(a,b)

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1, binary numerals in literal arithmetic.

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

keep DISPLAY;

updated;

renamed to Typedefs.thy to avoid conflict with main HOL version;

* proper spacing of consecutive markup elements, especially text blocks after section headings;

\newif\ifisamarkup controls spacing of isabeginpar;

improved spacing;

maintain Latex.flag_markup;

flag_markup;

Types/document/Typedefs;

renamed Typedef.thy to Typedefs.thy (former already present in main HOL);

got rid of separate root.tex;

graceful interpretation of -i/-d/-D options; verbose: additional messages/warnings; include document graph;

include document graph;

document graph option;

conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;

added TextIO.stdErr;

include document graph; tuned;

document graphs for several sessions;

tuned;

calculational rules moved from FOL to IFOL;

option -g for document graph; removed all presumptions about -d/-D (handled by isabelle process);

option -q also excludes -v true in generated stuff; tuned message;

dvips -q;

removed -v option (handled by isabelle process);

-o pdf: produce *both* eps and pdf; tuned;

* greatly simplified document preparation setup, including more graceful interpretation of isatool usedir -i/-d/-D options, and more instructive isatool mkdir; users should basically be able to get started with "isatool mkdir Test && isatool make"; * theory dependency graph may now be incorporated into documents; isatool usedir -g true will produce session_graph.eps/.pdf for use with \includegraphics of LaTeX;

got rid of ML proof scripts;

induct_method.ML -- proof by cases and induction on sets and types (Isar);

latex output: bold lambda;

got rid of ML proof scripts for Product_Type;

got rid of Provers/split_paired_all.ML;

improved default dependencies;

revert to proper version (!);

GPLed;

tuned;

use abstract product type instead of datatype;

moved atomize stuff to theory HOL;

legacy interfaces for axclass instantiation;

added map_base;

sane internal interfaces for instance;

sane internal interface for add_typedef(_i);

proper setup for abstract product types;

moved InductMethod.setup to theory HOL;