add new makefile dependencies

prove isomorphism and isodefl rules

avoid using csplit; define copy functions exactly like the current domain package

merged

remove one_typ and tr_typ; add abs/rep lemmas

automate definition of rep/abs functions

get rid of numbers on thy variables

automate proofs of REP equations

cleaned up; factored out fixed-point definition code

automate solution of domain equations

removed fixme - quick-and-dirty flag is appropriate

use of thm-antiquotation

Added new counterexample generator SML_inductive for goals involving inductive predicates.

Added infrastructure for embedding random data generators into code generated for inductive predicates.

unused_thms: show only results from 'theorem(s)' package (via old-style kinds); misc tuning -- slightly less hermetic names;

future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;

toplevel pretty printer for Synchronized.var;

adapted Local_Theory.define -- eliminated odd thm kind;

Specification.definition: Thm.definitionK marks exactly the high-level end-user result;

Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;

merged

merged

Minor correction

some attempts to improve termination of isatest;

Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS

Renamed vector_less_eq_def to the more usual name vector_le_def.

merged

replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules

concealing internal definitions of primrec specifications

adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler