Removed superfluous HOL/Matrix/cplex/ROOT.ML.

further simplification of the Isabelle-ATP linkup

added make function

removed some deprecated assocation list functions

introduced AList module

simplification of the Isabelle-ATP code; hooks for batch generation of problems

update usage message

obsolete;

converted to Isar theory format;

converted to Isar theory format;

converted to Isar theory format;

tuned;

converted to Isar theory format;

moved quick_and_dirty to Pure/ROOT.ML;

pretty_thm_aux: ora masked by quick_and_dirty;

added quick_and_dirty (from Isar/skip_proofs.ML);

manually generated from Isabelle/HOLCF/IOA/Complex/Import;

tuned document;

tuned;

added with_charset: string -> ('a -> 'b) -> 'a -> 'b;

tuned comments;

pretty_thm_aux: aconv hyps;

removed obsolete BasisLibrary; proof_general.ML: setmp proofs 1 to capture sane default preferences;

Hebrew: HTML.with_charset;

removed obsolete BasisLibrary;

added quickcheck_params (from Main.thy);

removed spurious PolyML.exception_trace;

moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);

minor cleanup, moved stuff in its proper place;

generate: added HOL-Complex-Generate-HOLLight;

added code generator setup (from Main.thy);

lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?

HTML.with_charset;

converted to Isar theory format;

tuned document;

obsolete;

plain test session, includes example;

theory_to_proof: check theory of initial proof state, which must not be changed;

added auto_fix (from proof.ML); added assms_of; removed assumptions_of; pretty_thm: show out-of-context hyps; warn_extra_tfrees: works again, tuned;

export put_facts; moved auto_fix to proof_context.ML; generic_goal: solve 0 subgoals initially; global_goal/theorem: only store results if SOME target, which may be empty;

interpretation: use goal commands without target -- no storing of results;

theorem(_i): empty target; forget_proof: removed tmp hack;

pretty_thm_aux: observe asms context;

tuned;

Cube: converted to Isar, use locales;

1) mapped .. and == constants 2) improved protect_varname

use interpretation command

add HOLCF entries for pcpodef, cont_proc, fixrec; add HOL-Complex entry for transfer tactic; clean up lists of theories in HOL-Complex entries

converted to Isar theory format;

fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions

add header

tuned

interpretation uses primitive goal interface

tuned

PARTIAL conversion to Vampire8

catching exception Io

rearranged

use mem operator

fix names in hypreal_arith.ML

merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy

merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up

add header

The SMLNJ Problem fixed...

getting it work for SMLNJ

* Improved efficiency of the Simplifier etc.;

incorporated into NEWS;

incorporated HOL/Hyperreal/CHANGES;

massive tidy-up and simplification

moving Commutative_Ring to the correct theory

comment

poly -doDisplay;

TableFun/Symtab: curried lookup and update; add_defs etc.: use Thm.get_axiom_i, which is independent from naming;

TableFun/Symtab: curried lookup and update; nat_option trace_simp_depth_limit;

fixed type;

fixed ML;

The Hebrew Alef-Bet -- Unicode example;

added Hebrew.thy;

TableFun/Symtab: curried lookup and update;

fixed document;

added HOL/ex/Hebrew.thy; tuned;

obsolete;

command 'thms_containing' has been discontinued in favour of 'find_theorems'; TableFun/Symtab: curried lookup and update; tuned;

Revert previous attribute name change, problem can be avoided in JAXB.

forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;

extend: NameSpace.default_naming;

the experimental tagging system, and the usual tidying

Change PGIP attribute name class->messageclass to avoid Java keyword clash.

AList, the_*

fixed type annotation

added gen_list to Pretty module

@{term [source] ...} in subsections probably more robust;

tuned;

hide: added option '(open)';

imports Commutative_Ring instead of Main, since the latter hides our names;

hide the rather generic names used in theory Commutative_Ring;

renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;

... prem19

added prem10 - prem19

removed syntax fun_map_comp; introduced map_comp;

Unfortunately patched to use IntInf.int instead of just int (SML compatibility)

Method comm_ring for proving equalities in commutative rings.

tuned headers etc.;

fixed some ML names;

imports Commutative_Ring;

HOL: method comm_ring; Proof General: Unicode (UTF-8) support;

tuned;

no longer prefer xemacs, which fails more often than GNU emacs;

Bernhard Haeupler: comm_ring;

tactic and the rest eliminated, just the theory....

use was wrong...

Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.

The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring

introduced AList.lookup

correct E brackets

nice names for more infix operators

introduces AList.lookup

removed duplicated lemmas; convert more proofs to transfer principle

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;

converted to Isar theory format;

obsolete (see Cube.thy);

tuned msg;