fixed a failing proof

le_refl_iff as default rule

removed needless premises

AddIffs now available for FOL, ZF

added simp_case_tac; proper handling of case names with simplification; support "(opaque)" mode; tuned;

use InductMethod.simp_case_tac;

tuned;

export thesisN separately;

prep rhs in original context; tuned;

RuleCases.make opaq;

bind_skolem;

invoke_case: bind_skolem;

"_i" arguments now expected to have skolems already internalized; removed unused cert_skolem, export intern_skolem, added bind_skolem;

make: opaq flag;

added internal, dest_internal;

infix 'OF' is a version of 'MRS' with more appropriate argument order;

about.html -> logics.html

munich webserver is now sunbroy51

about -> logics, better access to online libraries

removal of (harmless) circular definitions

Tuned proof.

Defs are now checked for circularity (if not overloaded).

inter_sort: keep normal!

Tightened up check of types in constant defs.

added type classes to constant's type

skp; le;

added dependency caveat

added dependency caveat

added IMP/Examples.ML dependence

tuned msgs;

allow comment in more commands;

Isabelle99-1;

ADD -> IAdd

Removed some junk thms.

added zabs to arith_tac

Deleted list_case thms no subsumed by case_tac

Now two split thms for same constant at different types is allowed.

removal of batch style, and tidying

removal of batch style, and tidying

removal of batch style, and tidying

removal of batch style, and tidying

removed sorry;

removed sorry;

new ADD instruction

removal of batch style, and tidying

fixed typos reported by Jeremy Dawson

added;

completed TYPES version of HahnBanach;

*** empty log message ***

Compatibility file for Moscow ML 2.00;

run Moscow ML 2.00 --- does not handle saved images (yet!?);

Moscow ML 2.00 or later (experimental!); tuned;

more tidying. also generalized some tactics to prove "Type A" and "a = b : A" judgements

disambiguated := ; added Examples (factorial)

removed batch proofs

massive tidy-up: goal -> Goal, remove use of prems, etc.

disambiguated := ; added Examples (factorial)

corrected symbol for casting relation

removed most batch-style proofs

tuned;

disambiguated := ; added Examples (factorial)

added a thm.

disambiguated := ; added Examples (factorial)

added BinOp

* added 'nothing' --- the empty list of theorems;

added "nothing" (empty list of theorems);

fixed usage;

tuned comments; even smarter guessing of ProofGeneral location;

previde 'defs' field for quick_and_dirty;

IGNORE last log message! added antiquote options "long_names", "eta_contract";

removed "help";

added no_vars att;

eta_contract: no default;

GPLed;

* Isar/HOL/Calculation: new rules for substitution in inequalities (monotonicity conditions are extracted to be proven terminally);

added subst rules for ord(er), including monotonicity conditions; name all rules; tuned;

added ISABELLE_SITE_SETTINGS_PRESENT;

tuned;

added site settings check;

* Isar: removed 'help' command, which hasn't been too helpful anyway; should instead use individual commands for printing items (print_commands, print_methods etc.);

removed help; added print_commands;

removed help_methods; tuned print_methods;

removed "help"; added "print_commands", "print_trans_rules", "print_antiquotations";

added options "eta_contract", "long_names"; tuned print_antiquotations; removed help_antiquotations; tuned;

added print_trans_rules, print_antiquotations;

removed help;

tuned print_rules;

removed help_attributes;

print_theorems: omit name space;

Defined abs on int.

help_antiquotations;

overloading, axclasses, numerals and general tidying

removal of batch-style proofs

more tidying

presentation: self-contained session dirs;

fixed ISABELLE_BROWSER_INFO;

removed the mutual recursion from "bin_add"

tidied and deleted two redundant theories NB Misc lemmas needed in personal developments should not be added to HOL

improved arrangement of files; tuned;

tuned rail setup; some isabelle symbols;

added lbrace, rbrace, atsign;

added \indexisarant;

adapted args of IsarThy.have_theorems_i;

syntax: renamed 'thmname' to 'thmbind'; added subsection{Antiquotations};

facts: support multiple lists of arguments; method_setup command;

* formal comments (text blocks etc.) in new-style theories may now contain antiquotations of thm/prop/term/typ to be presented according to latex print mode; concrete syntax is like this: @{term[show_types] "f(x) = a + x"}; * Isar: theory command 'method_setup' provides a simple interface for definining proof methods in ML;

added method_setup; facts: handle multiple lists of arguments;

facts: handle multiple lists of arguments;

fixed is_semicolon (keyword instead of command!);

added add_method;

have_theorems etc.: handle multiple lists of arguments; added method_setup;

have_thmss: handle multiple lists of arguments;

now freezes Vars in order to prevent errors in cases like these: Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx"; Goal "Suc (x + i + j) = x + f(?q i j) + k"; Goal "Suc (x + i + j) = x + ?q i j + k"; Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";

tidied proofs using default rule equalityCE

the default equalityCE simplifies proofs

tidied

fixed proof to cope with the default of equalityCE instead of equalityE

now uses equalityCE, which usually is more efficent than equalityE

weak elimination rules

classical 'elimify' attribute;