improved exhibit_interrupt;

\isamath and \isatext: more abstract implementation of symbols;

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

fixed \isastyleminor for "tt": \small;

*** empty log message ***

*** empty log message ***

fixed 'clarify': CHANGED;

fully enclose "\isadigit{...}"; \<^foo> produces "\isactrlfoo ";

tuned;

AddXEs [someI_ex];

added a section label

fixed hrefs: index.html;

added rtranclIs

*** empty log message ***

*** empty log message ***

tuned text;

ex_someI -> someI_ex

simplified rtrancl_converse{I,D}

got rid of a swap

expandshort

*** empty log message ***

@ -> SOME

tuned;

final tuning;

tuned;

tuned;

tuned;

* HOL/IMPP: extension of IMP with local variables and mutually recursive procedures, by David von Oheimb;

updated, improved;

tuned;

draft for 99-1;

tuned;

*** empty log message ***

tuned;

* HOL/Lattice: fundamental concepts of lattice theory and order structures;

Updated README file for HOL/Real

new 'THEN' syntax;

tuned;

added more stuff;

improved @;

'THEN', 'COMP': improved optional position arg;

added "bracks";

*** empty log message ***

Hoare logic in Isar;

tuned deps;

tuned;

added Hoare;

hide declaratations;

added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;

unsymbolized;

tuned names; added more theorems of group theory (from old AxClasses/Group/Group.ML);

major cleanup -- improved typesetting;

unsymbolize;

eliminated \<oplus>;

removed "symbols" syntax for constant "override";

reorganized AxClasses;

reorganized AxClasses;

moved axclass tutorial examples to top dir;

*** empty log message ***

updated;

range declared as syntax;

added == transitive rule (bad idea??);

improved t.weak_case_cong text;

delcongs weak_case_congs;

renamed "None" to "NONE" (avoid clash with option type);

qed "";

tuned;

*** empty log message ***

*** empty log message ***

*** empty log message ***

export get_datatypes_sg; added weak_case_congs_of(_sg);

info: weak_case_cong;

separated expr and stmt

isapar: \medskip;

Now some functions try to avoid name clashes when introducing new free variables.

tuned;

tuned;

tuned;

include log files;

tuned;

some preliminary stuff on conversion;

fixed ref;

record proof tools: t.equality; inductibe: split_asm, splits, cases; tuned;

isabelle -C;

www.proofgeneral.org;

fixed \<Union>, \<Inter> syntax;

added COPYDB argument;

option -C;

Isabelle99-1 (October 2000);

support copy option;

./build -b -m Pure-copied Pure;

only run quick_and_dirty version by default;

tuned;

deleted card_0_empty_iff because it is the same as card_0_eq; renamed some variables

THIS_IS_ISABELLE_BUILD;

tuned;

tuned comment;

proper Hyperreal setup;

more symbolic syntax (currently "input");

exchanged the declaration of "seealso" and loading of "makeidx" because the latter redeclares this macro

tuned;

FAKE_BUILD="";

updated;

updated;

tuned;

replaced by document (cannot maintain both);

simplified; got rid of rpm;

weblint;

got rid of RPM;

make Isabelle logic images for current platform;

simplified;

HOL/MicroJava;

www.proofgeneral.org;

updated url;

tuned;

removed the obsolete (and badly named) inj_select Added new theorems about Compl, image, bij/inj/surj

tuned;

tuned;

tuned;

tuned;

tuned replacements;

tuned auto paths;

untabified for HTML

include "Isabelle" link;

tidied, removing obsolete "goal" commands

new theorems and comment

renaming the inverse image operator in HOL

added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.

tuned comments;

AddXIs [equal_intr_rule];

added HTML syntax; added spaces in normal syntax for better documents

added HTML syntax

removed JVM/Store.ML, added theorem Digest in MicroJava

lemma now in Store.thy

converted to Isar, tuned

tuned spacing for document generation

*** empty log message ***

renamed to Records.thy;

improved \isachartilde for non-tt styles;

renamed HOL/ex/Points to HOL/ex/Records;

added height="100%" to stretch page to whole browser window

added headline, "quick download", and mailing list archive

added height="100%" to stretch page to whole browser window

*** empty log message ***

Digest.thy as toplevel theory

theorem digest of all MicroJava theorems, theories in alphabetical order may also serve as toplevel file that includes all other theories

New theories: construction of hypernaturals, nonstandard extensions, and some nonstandard analysis.

tuned, added lightweight BV to abstract, added Bali link

Updated Files with new theorems

unsymbolized

removed dead code;

added "install" target;

tuned;

tuned rpm command lines;

updated;

made SML/NJ happy;

added common args keywords;

tuned args;

added iff_add_global', iff_add_local' (syntax "iff?"); tuned;

tuned;

attribute / modifier 'iff': support "?" mode;

tuned msg;

updated;

tuned;

tuned;

remove unreadable symbol names from sources;

tuned;

added plain "tt" style;

*** empty log message ***

rpm --force;

best-style made default;

tuned;

tuned;

tuned;

include ANNOUNCE;

improved pages;

indicate occurrences of 'handle _';

removed -x option;

made SML/NJ happy;

AddXIs [prod_eqI];

AddXIs [ext];

added print_thm(s)_sg;

begin_theory: removed message;

Display.pretty_thm_sg;

isar-strip-terminators;

tuned;

updated;

safe_asm_full_simp_tac is back (for compat);

cleaned up and prepared for Isabelle99-1;