renamed Position.path to Path.position; added line_file, ignore empty name;

renamed Position.path to Path.position;

load seq.ML and position.ML earlier;

adapted PolyML.compiler to latest change of basis/FinalPolyML.sml (2008-04-21);

fixed makefile

NEWS about measure functions

updated generated file;

Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.

misc tuning;

updated generated file;

fixed some labels;

avoid old macros from isar.sty;

misc reorganization;

added chapters for "Specifications" and "Proofs";

removed outdated comment;

updated generated file;

proper antiquotations for commands;

removed obsolete macros for Isar commands etc.; tuned;

replaced macros by antiquotations;

removed obsolete macros for Isar commands etc.;

added local copy of underscore.sty;

updated generated file;

replaced some latex macros by antiquotations;

removed obsolete macros; tuned;

removed obsolete math macros;

depend on style.sty;

updated generated file;

depend on ../../antiquote_setup.ML;

improved treatment of "_" thanks to underscore.sty;

clean_string: map "_" to "\\_" (best used with underscore.sty);

misc tuning;

slight tuning of the 1st paragraph

unused;

converted HOL specific elements;

added rail setup for verblbrace, verbrbrace;

added at_set_avoiding lemmas

removed obsolete conversion guide -- converted only section on tactics;

converted ZF specific elements;

enabled ThyOutput.source option by default;

output_entity: ignore ThyOutput.source option;

updated generated file;

converted HOLCF specific elements;

added logic-specific sessions;

Updated.

Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.

Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.

Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).

Lookup and union operations on terms are now modulo eta conversion.

Terms returned by decomp are now eta-contracted.

Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.

eq_assumption now uses aeconv instead of aconv.

- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv

Replaced Pattern.eta_contract_atom by Envir.eta_contract.

Removed instantiation for set.

Explicitely applied ext in proof of tnd.

Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.

- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.

Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.

Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.

Functions get_branching_types and get_arities now use fold instead of foldl/r.