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