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;

tuned for ProofGeneral 3.2

tuning, eliminated rev_surj

fixed some weak elim rules, and tidied

tidying and unbatchifying

no longer depends upon a prior "open Ind_Syntax" from elsewhere

fixed some weak elim rules, and tidied

fixed some weak elim rules

simplified slightly by using dependencies better in theories

finally theory Bin (the integers) is included

FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG

fixed some weak elim rules

implements a classical version of make_elim

uses a supplied version of make_elim for addDs

warns of weak elim rules and ignores them

tidying and unbatchifying

fixed some abuses of addDs and addEs

got rid of weak elim rule

tidied

fixed some weak elim rules

make_elim -> cla_make_elim; tidied

updated and tidied

tidied a monstrous proof

deleted a redundant bind_thm

using the new theorem wf_not_refl; tidied

rev_notE now makes strong elim rules; tidied the file

declaring and using cla_make_elim

new file Provers/make_elim.ML

replaced arities by instance;

OuterLex.name_of: include val;

excursion_result: transform_error;

eq_prop: eta contract;

tuned msg;

tuned;

avoid \< in input;

export proper induction rule;

bind_thm;

corrected specifications and simplified proofs

isar-strip-terminators;

updated;

tuned;

use with_paths;

prefer mp over subst; tuned;

tuned;

Isar theory output.

Theory headers (old and new-style).

Text with antiquotations of inner items (terms, types etc.).

use Library.change;

adapted to improved presentation; no longer mirror items from structure Latex;

adapted to improved presentation;

excursion_result;

added extern_skolem;

moved header stuff to thy_header.ML; moved theory presentation to isar_output.ML; major cleanup;

added semicolon; added arguments; tuned;

added !!!; added is_semicolon; export incr_line, keep_line, scan_blank, scan_string; added source_proper; added make_lexicon; tuned;

use ThyHeader.args; adapted OuterSyntax.markup_command;

rearranged print commands;

exception OUTPUT_FAIL of (string * Position.T) * exn (*note: actually belongs to isar_output.ML*);

removed obsolete "{}";

added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;

added IsarOutput (token-level theory output);

added exhausted: ('a, 'b) source -> ('a, 'a list) source;

added state: 'a * 'b -> 'a * ('a * 'b);

fbrk: 2 if not taken;

export hidden: string -> string;

tuned;

added change: 'a ref -> ('a -> 'a) -> unit;

Added new theory Lambda/Type.

get_inductive now returns None instead of raising an exception.

Added new theory.

Subject reduction and strong normalization of simply-typed lambda terms.

new theorem trans_O_subset

added the AllocImpl example

genPrefix_trans_O: generalizes genPrefix_trans

added the allocator refinement proof

sum_below f n -> setsum f (lessThan n)