add theorem chain_const

tuned;

global quick_and_dirty;

Printing of Isar proof elements etc.

Non-empty stacks.

IsarThy.begin_theory;

export ml_exts;

begin_theory: tuned interface, check uses;

replaced TRANSLATION_FAIL by EXCEPTION;

added three_buffersN, print3; tuned theory_to_proof: plain Proof.state instead of history; added EXCEPTION; removed DATA_FAIL, TRANSLATION_FAIL;

load before proof.ML; moved proof elements to proof.ML;

added simple; eliminated obsolete Sign.sg;

added add_view, export_view (supercedes adhoc view arguments); unified put_thms/reset_thms;

major cleanup of interfaces and implementation; generic goal commands: local/global_goal with after_qed; independent of locale.ML; more self-contained proof elements (material from isar_thy.ML); refer to ProofDisplay (cf. proof_display.ML); unified print_results (always normal); added get_thmss;

added name_facts;

tuned Isar proof elements;

added cheating, sorry_text (from skip_proofs.ML); added method_setup (from isar_thy.ML);

load late, after proof.ML; added goal commands: theorem, interpretation etc.; tuned some warnings -- single line only;

moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.); begin_theory: tuned interface, check uses in thy_info.ML;

cleanup parsers and interfaces;

Proof.get_thmss;

tuned;

more self-contained proof elements (material from isar_thy.ML); tuned;

added cases, rule_contextN; eliminated obsolete Sign.sg;

load locale.ML late (after proof.ML); tuned module arrangement;

added maps, map_list, lift, lifts;

added stack.ML;

added simple_fact; generalized no_attributes;

Seq.maps;

added hide_names(_i) (from isar_thy.ML);

added generic_setup, add_oracle (from isar_thy.ML);

added exception EXCEPTION of exn * string;

replaced DATA_FAIL by EXCEPTION;

tuned Isar interfaces; tuned IsarThy.theorem_i;

added General/stack.ML, Isar/proof_display.ML;

the_list (cf. Pure/library.ML);

tuned IsarThy.theorem_i;

fixed INST: has same semantic now as INST_TYPE for repetitions

list of constants and theorems whose names have been changed or merged

add header

added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging

updated to work with latest HOL-Complex

add file Hyperreal/transfer.ML

new implementation of transfer principle

removed clutter

name conflict with global itrev resolved

dealt with name clash with List.itrev

introduced new-style AList operations

introduced internal function hthm2thm

1) Added target HOL-Complex-Generate-HOLLight 2) Make heap image for HOL-Complex-Matrix

Added HOLLight support to importer.

added interact flag to control mode of excursions;

excursion: interactive if debug;

updated to work with new HOL-Complex version

starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.

Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying

fixed printing of locales

consolidation of duplicate code in Isabelle-ATP linkup

introduces some modern-style AList operations

added the_list, the_default

yet more tidying of Isabelle-ATP link

converted to Isar theory format;

converted to Isar theory format;

converted to Isar theory format;

removed TLA/Inc/Pcount.thy;

elimination of watcher.sig

Progress on eprover linkup, also massive tidying

axioms now included in tptp files, no /bin/cat and various tidying

consolidation of watcher.ML and watcher.sig

generalized types more

generalized types

added theorem hypreal_inverse2

replace type hcomplex with complex star

replace type hypnat with nat star

replace type hypreal with real star

add Hyperreal dependencies

class instances for nonstandard types

transfer principle tactic

generic nonstandard type constructor

converted to Isar theory format;

fix proof

converted to Isar theory format;

reimplement Filter.thy with locales

converted to Isar theory format;

converted to Isar theory format;

removed some ML files in Modelcheck/;

updated;

axclass: no longer bind "cI";

deprecated old-style infix declarations, which mix name and syntax;

tuned msg;

AList.defined;

name space prefix is now "c_class" instead of just "c"; export get_info; tuned;

proper treatment of polymorphic sets; tuned;

tuned comments;

converted to Isar theory format;

make LocalesTest last, because it sets funny flags;

avoid old-style infixes;

axclass: name space prefix is now "c_class" instead of just "c"; typedef: proper support for polymorphic sets;

axclass: name space prefix is now "c_class" instead of just "c";

unnecessary parentheses removed

converted to Isar theory format;

introduced some new-style AList operations

eliminated 1 call to polyEq

tuned;

updated;

obsolete;

added assert, command;

tuned check_text;

chapter/section/subsection/subsubsection/text: optional locale specification;

markup commands: optional locale specification;

add_chapter/section/subsection/subsubsection/text: optional locale specification;

curried_lookup/update;

tuned;

Markup commands 'chapter' .. 'text' support optional locale specification;

removed duplicate theorems;

introduced binding priority 1 for linear combinators etc.

converted to Isar theory format;

tuned method;

tuned;

obsolete;