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.