fixed presentation

Removed mult_commute axiom from comm_semiring axclass.

compilation error fixed

support for recursion over mutually recursive IDTs

Cleaned up, now use interpretation.

Cleaned up, now uses interpretation.

deleted obsolete code

Interpretation supports statically scoped attributes; documentation.

updated;

added delete_safe, insert, remove, remove_multi; tuned;

clarified insert/remove; tuned canonical fold/fold_rev;

tuned;

binds/thms: do not store options, but delete from table; tuned;

tuned comments;

removed;

expect translations functions to be stamped already; added remove_const_gram;

added stamp_trfun, mk_trfun, eq_trfun;

tuned extend_prtabs; added remove_prtabs;

added make_gram; merge_gram: do not add chain productions to prods;

identify binder translations only once (admits remove);

Syntax.mk_trfun;

tuned (t)inst_tab_elem;

added 'no_syntax' command;

added del_modesyntax(_i);

added del_modesyntax(_i); added print_all_data;

added gen_remove, remove; usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;

Pure: command 'no_syntax' removes grammar declarations;

removed;

speed improvements for the domain package

New file for theorems used by the domain package

rermoved pointless example

yet more tidying up: removal of some references to Main

*** empty log message ***

New

more tidying up of the SPASS interface

Removed most of the atp interface from Pure.

Include automatic determination of poly version.

Add RDISTDIR option used by Isabelle RPM.

Added thm names

Removed dir Orderings in Library

fix: added path to garbage

added LaTeXsugar

added Makefile and generated files to make document available for makedist

Locales: proper static binding of attribute syntax; Attributes 'induct' and 'cases': support local type or set names;

*** MESSAGE REFERS TO PREVIOUS VERSION *** support embedded values and static binding -- via implicit assignment to src tokens (cf. assignable/assign/closure); renamed ident/string/keyword to mk_ident/mk_string/mk_keyword; added mk_name, mk_typ, mk_term, mk_fact, mk_attribute; added type value with map_values etc.; removed name_dummy, added general 'maybe' combinator; added global/local_tyname/const; added pretty_src, pretty_attribs; added thm_sel (from attrib.ML);

*** MESSAGE REFERS TO PREVIOUS VERSION *** added read_tyname/const;

*** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT setting specifies preferred document format; some cleanup;

*** MESSAGE REFERS TO PREVIOUS VERSION *** added declared_tyname/const and read_tyname/const; removed certify_tyname/const; added prep_ext_merge, nontriv_merge kept internal; efficient subsig test;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; removed Locale.multi_attribute (pass Attrib.src instead); removed interpret(_i) (use have_i instead); goals: more uniform treatment of after_qed, removed separate thy_mod of global goals;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed type multi_attribute (store Attrib.src instead); datatype elem/element(_i): Attrib.src instead of 'att; removed map_attrib_element etc.; added intern_attrib_elem(_expr); added map_elem, map_values to economize code; static binding of values in Attrib.src (cf. Args.closure, Attrib.crude_closure); prep_facts: transfer internal facts;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src, Method.src; Sign.declared_tyname/const; no Attrib.multi_attribute, pass Attrib.src directly to locales; register_locally: Proof.interpret_i replaced by Proof.have_i;

*** MESSAGE REFERS TO PREVIOUS VERSION *** type src = Args.src; renamed local_attribute' to context_attribute; added _i versions of global/local/context_attribute and separate intern/intern_src; added crude_closure to produce argument closure without knowing facts in advance; added 'attribute' to embed internal attributes into src; removed multi_attribute etc.; moved thm_sel to args.ML; Scan.peek; read_instantiate/'where'/'of': support arbitrary mix of external / internal typ / term args, with proper treatment of static binding;

*** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT; tuned;

*** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Sign.prep_ext_merge;

*** MESSAGE REFERS TO PREVIOUS VERSION *** added datatype interval, improved thm selections;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed uterm, added 'maybe'; Attrib.src; improved thm_sel;

*** MESSAGE REFERS TO PREVIOUS VERSION *** type src = Args.src; Drule.add_used;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed uterm; tuned;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; ISABELLE_DOC_FORMAT;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Scan.peek; Args.global/local_const/tyname (static binding!);

*** MESSAGE REFERS TO PREVIOUS VERSION *** use args.ML, attrib.ML earlier;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Scan.peek; Args.local_tyname, Args.local_const;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Method.src;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Args.global_const (static binding!);

*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;

*** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; Args.maybe;

*** empty log message ***

new signalling primmitives for sml/nj compatibility

*** empty log message ***

tweaks mainly to achieve sml/nj compatibility

fixing an incompatibility with Posix.IO.mkTextReader

auto update

removal of Main and other tidying up

First release of interpretation commands.

tuned

added \restriction

tuned Map, renamed lex stuff in List.

Added lots of AMS harpoons

_(_|_) is now override_on

tuned

section on qmark

fixed the syntax of infix declarations

thmref: selection syntax;

update syntax of 'where' and 'of';

added PDF_VIEWER, ISABELLE_DOC_FORMAT;

Reconstruction code, now packaged to avoid name clashes

temporarily removed ATP code

removed bad code

Changed prob1.dfg to prob_1.dfg

Got rid of Main.thy reference

Integrating the reconstruction files into the building of HOL

Reconstruction.thy and IsaMakefile updated

*** empty log message ***

new meta-level rules

*** empty log message ***

reverted renaming of Some/None in comments and strings;

added term_8;

added get_axiom_i, invoke_oracle_i;

Drule.add_used;

invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!

added add_used; include tpairs;

improved exn_message;

Thm.invoke_oracle_i;

Scan.peek;

tuned updates, added map_entry;

added some, peek, trace'; tuned;

added header;

improved comments;

reverted renaming of Some/None in comments and strings;

handle Option instead of OPTION;

updated it

watcher.ML and watcher.sig changed. Debug files now write to tmp.

Current version of res_atp.ML - causes an error when I run it. C.Q.

lexicographic order by Norbert Voelker

arg_cong2 by Norbert Voelker

*** empty log message ***

Updated to add watcher code.

CVSfj  ------------------------------------------------------------------- --------------------------------------------------------------- Temporarily added until res_axioms.ML is altered.

Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.