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;