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;

setup generic cases and induction (from Inductive.thy);

guillemot syntax;

improved internal interface of typedef;

abstract product types;

proper proof of split_paired_all (presently unused);

tuned comments;

added mk_UNIV;

tuned;

simplified exporter interface;

added implies_intr_goals;

tuned;

Tuned.

Removed exit command from end of main method.

PS method now calculates layout using default font metrics.

Inserted table for character widths.

tuned induction proofs;

dest_env: norm_term on rhs;

typedef: export result;

ignore typedef result;

declare projected induction rules stemming from nested recursion;

TypedefPackage.add_typedef_no_result;

tuned;

* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);

option -o FILE --output to FILE (ps, eps, pdf);

ISABELLE_EPSTOPDF="epstopdf";

Font metrics used for batch mode layout (without X11 connection).

Added support for batch mode layout (without X11 connection).

tuned;

improved induct;

be more careful about token class markers;

proper order of kind names;

support impromptu terminology of cases parameters;

parser for underscore (actually a symbolic identifier!);

allow empty set/type name;

simplified resolveq_cases_tac for cases, separate version for induct; divinate instantiation of induct rules; tuned;

tuned;

canonical 'cases'/'induct' rules for n-tuples (n=3..7)

canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)

setsum syntax;

intro! and elim! rules;

tuned NetRules;

Tactic.orderlist;

ObjectLogic.rulify;

Tactic.rewrite_cterm;

GPLed;

ring instead of ringS;

ring includes plus_ac0;

tuned;

support weight;

bang_args;

qualify some names;

map_nth_elem;

renamed reset_locs to del_locs

moved rulify to ObjectLogic;

moved rulify to ObjectLogic;

added qed_spec_mp etc.;

unified rewrite/rewrite_cterm/simplify interface;

tuned rewrite/simplify interface;

improved atomize setup;

atomize_tac etc. moved to object_logic.ML;

use ObjectLogic;

added 'atomize' attribute;

tuned full_rewrite;

ObjectLogic.setup;

tuned;

added object_logic.ML;

fixed auto steps (due to changed atomize);

Specifics about common object-logics.

use ObjectLogic stuff;

"HOL.mono";

ObjectLogic.atomize_tac;

improved atomize setup;

removed Ord;

removed Ord.thy (now part of HOL.thy).

judgment Trueprop; proper declarations of atomize rules; incorporate theory Ord; proper section and text markup; tuned;

added ML bindings from former theory Ord;

eliminated atomize rules;

judgment Trueprop; proper declarations of atomize rules;

updated;

* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

'morphisms' spec; tuned goal pattern for set;

tuned;

generic theorem kinds;

generic theorem kinds ("theorem", "lemma" etc.);

IsarThy.theorem_i Drule.internalK;

Drule.tag_internal;

* Pure: added 'corollary' command;

Tuned comment.

- Exported goals_conv and fconv_rule - Added forall_conv

removed vars_of, concls_of; removed additional rule instantiation argument; proper enumeration of type rules; append possibilities of set and type rules (analogous to elim-intro in 'rule');

declare impE iffD1 iffD2 ad elim of Pure;

removed lookups count; always try headless rules;

added make_thm (sort-of);

added trace_rules, trace;

removed get_cases, get_induct; added find_cases[ST], finde_induct[ST]; proper indexing of types;

removed read_inst', no longer export insts';

fixed typid;

test: use SkipProof.make_thm instead of Thm.assume;

tuned;

HOLogic.dest_concls, InductAttrib.vars_of;

declare impE iffD1 iffD2 as elim of Pure;

moved trace_rules to Pure/Isar/method.ML; some_rule_tac: prefer Method.some_rule_tac of Pure, no special handling of imp_elim;

* Isar/Pure: fixed 'token_translation' command;

added try;

added certify_tyname;

Exported output_symbols.

Removed unnecessary application of Drule.standard.

Fixed erroneous type constraint in token_translation function.

Exported output_with.

Tuned several functions to improve sharing of unchanged subproofs.

added global modes ref;

sane numerals (stage 3): provide generic "1" on all number types;

* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;

fixed numerals;

added tturnstile, TTurnstile;

*** empty log message ***

*** empty log message ***

replace 0r/1r by 0/1;

*** empty log message ***

fixed numerals;

* sane numerals (stage 2): plain "num" syntax (removed "#");

tuned;

*** empty log message ***

sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;

*** empty log message ***

"num" syntax;

added axclass "one" and polymorphic const "1"; print consts "0" and "1" with type constraints;

added "num" token;

induct: case names;

sane spacing of "-";

tuned;

Thm.major_prem_of part of Logic.strip_assums_concl;

major_prem_of: Logic.strip_assums_concl;

induct/cases made generic, removed simplified/stripped options;

improved proof by cases and induction;

removed obsolete comment;

generic induct_method.ML; tuned;

non-oriented infix = and ~= (output only); added case_split (with case names);

$(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;

use "~~/src/Provers/induct_method.ML";

removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);

added dest_concls;

simp_case_tac is back again from induct_method.ML; tuned;

made generic (see Provers/induct_method.ML);

qualify MetaSimplifier;

unsymbolized;

moved atomize stuff to theory IFOL; added induct/cases setup;

atomize stuff from theory FOL; tuned;

added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;

theory Natural_Numbers;

use "~~/src/Provers/induct_method.ML";

Theory of the natural numbers: Peano's axioms, primitive recursion. (Modernized version of Larry Paulson's theory "Nat".)

full_rewrite_cterm_aux (see also tactic.ML); no longer open MetaSimplifier;

added full_rewrite_cterm;

proof by cases and induction on types and sets (used to be specific for HOL);

qualify MetaSimplifier;

added dest_conj, dest_concls;

document setup;

added print_induct_rules;

tuned print operation;

tuned;

* moved induct/cases attributes to Pure, added 'print_induct_rules' command;

print_induct_rules;

updated;

Fixed bug in decompose.

Tools/induct_attrib.ML now part of Pure;

Isar/induct_attrib.ML;

*** empty log message ***

moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;

tuned parentheses in relational expressions;

moved linorder_cases to theory Ord;

linorder_cases supersedes linorder_less_split; tuned parentheses in relational expressions;

eta-expansion required for SML/NJ

support non-oriented infix;

tuned;

tuned;

*** empty log message ***

initial setup for chapter on document preparation;

updated output;

- declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This

Removed some unfoldings of defs after declaring wf_java_prog as syntax

Added axiom e~=This to reflect strengthened precond. in rule LAss

Minor modifications

added Ordinals example;

Tuned indentation of abstractions.

tuned;

inductive: no collective atts;

inductive: no collective atts;

oops;

tuned;

recdef (permissive); inductive: no collective atts;

*** empty log message ***

prove: ``strict'' argument;

internal thm numbering with ":" instead of "_";

avoid handle _;

permissive option;

inductive: no collective atts;

updated;

recdef (permissive);

Tuned section about parsing and printing proof terms.

mksimps and mk_eq_True no longer raise THM exception.

Added label for section on terms.

Added documentation for proof terms.

Added TYPE to Pure grammar.

Added \ttlbrack and \ttrbrack.

Added TPHOLs2000 paper about proof terms.

updated;

tuned;

tuned;

- Exchanged % and %%. - Fixed bug in shrink.

- Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information

- Exchanged % and %% - Renamed reconstruct_prf to reconstruct_proof

Exchanged % and %%.

HOL: eliminated global items;

updated;

eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");

renamed theory "subset" to "Typedef";

unsymbolize;

renamed "()" to Unity;

HOLogic.unit;

made unit type local;

tuned:

renamed "()" to Unity, made local;

added surjE;

prepared for Isabelle2001;

renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;

updated;

renamed real_of_int_eq_iff to real_of_int_inject;

document setup;

new-style theory;

Square roots of primes are irrational;

AddXIs [dvdI]; AddXEs [dvdE]; added dvd_mult_div_cancel;

tuned;

tuned;

tuned;

AddXEs [UnI1, UnI2];

AddXEs [disjI1, disjI2];

ex/Hilbert_Classical.thy ex/document/root.tex;

tuned;

document setup;

derive tertium-non-datur by means of Hilbert's choice operator;

obsolete;

updated;

-v option;

verbose option;

use_dir: verbose option;

removed option -d (now standard behaviour); added option -q; include notes;

option -v;

activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;

updated;

tuned order;

bold symbols;

tuned;