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;

converted to Isar theory format;

obsolete (see Cube.thy);

tuned msg;

uses ("LCF_lemmas.ML");

converted to Isar theory format;

tuned;

removed fix.thy, pair.thy, simpdata.ML; renamed LCF.ML to LCF_lemmas.ML;

converted to Isar theory format;

converted to Isar theory format;

setmp print_mode []; more robust outer syntax; tuned;

tuned;

simplified oracle;

use Check.ML;

fixed ML errors;

removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;

deprecated non-Isar theory file format;

Added ECommunication.ML

Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and recon_transfer_proof.ML to deal with the E theorem prover.

further tidying up of Isabelle-ATP link

converted specifications to Isar theories;

some 'assoc' etc. refactoring

tidying up the Isabelle/ATP interface

fixed arities and restored changes that had gone missing

deleted obsolete VampireCommunication.ML

print_locale omits facts by default

curried_lookup/update;

refrain from sorting output;

curried_lookup/update; removed obsolete current_sign; tuned;

curried_lookup/update;

curried_lookup/update; tuned;

added curried_lookup/update operations -- in preparation of currying plain lookup/update;

curried_lookup/update;

updated;

renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;

removed obsolete 'symbols' mode;

added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned;

improved formatting

isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;

updated;