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