*** empty log message ***

*** empty log message ***

isa-migrate ++

isa-migrate ++

isa-migrate ++

added macos emacs hints

isa-migrate ++

Domain package uses ContProc for beta reduction

allow theorem attributes on fixpat declarations

fixrec package now handles mutually-recursive definitions

(undone experimental changes)

subclassing done

int -> IntInf.int

added lemmas

*** empty log message ***

documented DUMMY

in domain declarations, selector names are now optional

use POLY instead of DISCGARB;

discontinued polyml-3.x; made cygwin functionality less intrusive; more quoting of expressions;

export cases_tac, induct_tac;

added type tactic;

int --> IntInt.int

renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda

cleaned up and reorganized

moved continuity simproc to a separate file

up_eq and up_less in default simpset now

internalize axiom names in Defs.define; compress types via Term.compress_type

downgraded to pdf v 1.4

experimental

just non_functional experimantal code, by now

changed -1 back to 0

more timing information

simp_depth now starts at -1 to make it start at 0 ;-)

added ML-Systems/polyml-posix.ML;

pass ml_platform;

Posix patches (from polyml.ML);

some cygwin support;

* Pure/sign/theory: discontinued named name spaces; * Pure: Theory.axioms_of, PureThy.thms_of etc.;

renamed hide_space to hide_names; refer to name spaces values instead of names;

renamed IsarThy.hide_space to IsarThy.hide_names;

name space of classes and types maintained in tsig;

renamed hide_classes/types/consts to hide_XXX_i; added separate hide_classes/types/consts; refer to name spaces values instead of names;

discontinued named name spaces (classK, typeK, constK); name space of classes and types maintained in tsig; read_tyname/read_const now raise ERROR instead of TYPE; tuned;

accomodate changed #classes; tuned;

accomodate changed #classes;

Theory.hide_consts renamed to Theory.hide_consts_i;

refer to name spaces values instead of names;

renamed Sign.intern_tycon to Sign.intern_type;

fixed spelling;

further optimizations of cycle test

tuned

tuning

IntInf change

All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG.

added Isar_examples/Drinker.thy;

full Display.pprint_theory for ML toplevel facilitates debugging;

simplified is_stale, check_stale; fixed map_sg -- proper treatment of non-drafts;

updated;

axioms: NameSpace.table;

PureThy.all_thms_of;

Theory.all_axioms_of, PureThy.all_thms_of;

can (Thm.get_axiom_i thy) name; removed duplicate code;

renamed extern to extern_thm; renamed cert/read_typ_raw to cert/read_typ_abbrev; added cert/read_typ_syntax; thms: NameSpace.table;

meths: NameSpace.table;

NameSpace.extern_table; ProofContext.extern_thm;

Args.local_typ_abbrev;

attribs: NameSpace.table;

renamed global/local_typ_raw to global/local_typ_abbrev;

added structure Inttab; tuned comments;

added type NameSpace.table with basic operations;

renamed cert_typ_raw to cert_typ_abbrev; renamed add_abbrs to add_abbrevs; tuned;

axioms and oracles: NameSpace.table; added axioms_of, all_axioms_of;

map_typ and map_term no longer global;

Major cleanup: got rid of types bclass, xclass, xsort, xtyp, xterm; reorganized code to separate stamps/data/sign; clarified name space inter/extern operations; sane read/certify operations -- more picky about stale signatures; sane implementation of signature extensions;

thms_of no longer global; added all_thms_of; theorems: NameSpace.table;

NameSpace.extern_table;

print_theory: omit name spaces; NameSpace.extern_table;

got rid of bclass, xclass;

add_axioms_infer -- avoids use of stale theory;

Theory.all_axioms_of;

Sign.read_typ_abbrev;

added chmod for packages

added CONTRIBUTORS

a very little cleanup

make up_eq and up_less into simp rules

Fixed "axiom" generation for mixed locales with and without predicates.

added some notes

added file acces rights handling

fix usage of inverts lemma, which has fewer premises now

faster proofs of inverts and injects lemmas, with fewer strictness hypotheses

fixed renamed lemma

major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas

added theorems is_ub_range_shift and is_lub_range_shift

added theorems less_sprod, spair_less, spair_eq, spair_inject

renamed theorems less_ssum4a,b,c,d to more meaningful names

added theorem less_cprod

added theorem injection_less

A flag DEFS_CHAIN_HISTORY can be used to improve the error message in case a cycle has been detected. If it is switched off and a cycle has been detected, the user is notified that there is such a flag.

extended readme

started migration framwork script

added basics for generic migration tool

added isatest-lint prototype

1) Fixed bug in Defs.merge_edges_1. 2) Major optimization of Defs.define: do not store dependencies between constants that cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to theories that define their constants in HOL-light / HOL4 style. 3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.

*** empty log message ***

updating...

Added the t = x "fix" - in (* ... *) :-(

copy_dir: be permissive wrt. errors;

integrated MacOS X installation instructions

(cvs removed)

migrated scripts to new webiste

minor refinements

Some error messages have been eliminated as suggested by Tobias Nipkow

junk

update -> use

refinements

Added code lemma for <

avoid polymorphic ins;

fixed (exited abnormally when ~/isabelle/etc/settings not present)

added sunbroy2

renamed const_deps to defs; improved error messages; major cleanup -- removed quite a bit of dead code;

renamed const_deps to defs; Type.freeze;

added Type.freeze(_type); tuned;

added the_const_type;

Type.freeze;

find empty dirs up to depth 5; tuned move of generated doc files; rm -f TODO;

DISCGARB_OPTIONS back in od position;

link bugs fixed

link bugs fixed

link bugs fixed

bugfix in record_type_abbr_tr'

added detection for GNU cp

added detection for GNU cp

symlink problem hopefully solved

better symlink handling

a more spohisticated symlink handling

a more spohisticated symlink handling

a more spohisticated symlink handling

added rsync symlink option

typo

added authors

replaced File.sysify_path by Path.pack; avoid "handle _" (which is not well-defined due to erratic Interrupt exceptions);

tuned msg;

File.isatool, File.shell_path;

present new-style theory header, with 'imports' and 'uses';

removed file_info (now in Pure/General/file.ML);

new Isar header: reject ':', accept both 'files' and 'uses'; tuned;

added 'uses' keyword;

removed copy, copy_all (superceded by File.copy, File.copy_dir); File.shell_path, File.isatool; tuned;

no warning for non-identifiers;

removed sysify_path, quote_sysity_path etc.; added platform_path, shell_path etc.; improved copy: support dir as target; added copy_dir; added isatool; tuned;

File.platform_path vs. File.shell_path;

File.platform_path;

File.shell_path;

added isatool version;

tuned/updated antiquotations;

updated theory header syntax;

DISCGARB_OPTIONS: proper treatment of specific polyml versions; the feeder is back (previous version did not really work with Isar.loop);

observe ISABELLE_IGNORE_USER_SETTINGS;

Lucas Dixon;

* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path; tuned;

#SMLNJ_CYGWIN_RUNTIME=1

added README

fixed links

fixed links

fixed links

fixed NEWS link

added library symlink

added library symlink

added library symlink

adjusted navigation width

added shellcmd style

added shellcmd style

added shellcmd style

added shellcmd style

re-added binary files

(temporary remove, forgotten the -b flag...)

major reorganization and cleanup;

added new website

added explicit dependency on Fix theory

add keywords fixrec and fixpat for HOLCF fixrec package

fix imports

use fixrec_package.ML

import Fix is unnecessary

added fixrec_package.ML

implementation of fixrec package

shrink session graph so it fits on a page

Domain package generates match functions for new datatypes, for use with the fixrec package

add dependency on Fixrec.thy

add Fixrec.thy

New theory with lemmas for the fixrec package

changed variable name in monofun_cfun_arg

fixed renamed theorems