use theory data for REP_simps and isodefl_rules

replace defl_tab and map_tab with theory data

separate conjuncts of isodefl theorem

automate isodefl proof

change example to use recursion with continuous function space

add lemma isodefl_cprod

automate definition of map functions; remove unused code

change naming convention for deflation combinators

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;