adding HOL-Mutabelle to tests

merged

more explicit naming scheme

merged

adapt to changed variable name in casedist theorem

remove dependency on domain_syntax.ML

update HOLCF makefile

simplify add_axioms function; remove obsolete domain_syntax.ML

proof scripts use variable name y for casedist

fixrec and repdef modules import holcf_library

use y as variable name in casedist, like datatype package

proper names for types cfun, sprod, ssum

variable name changed

fix proof script for take_apps so it works with indirect recursion

remove dead code

remove unused mixfix component from type cons

cleaned up, added type annotations

remove unused selector field from type arg

add_syntax no longer needs a definitional mode

add_axioms no longer needs a definitional mode

get rid of primes on thy variables

move definition of finiteness predicate into domain_take_proofs.ML

move take-related definitions and proofs to new module; simplify map_of_typ functions

remove map_tab argument to calc_axioms

remove dead code

merged

Slightly generalised a theorem

merged

merged

merged

merged

merged

merged

Correction of a tiny error

removed obsolete helper theory

merged

dropped superfluous naming

UNIV is not a logical constant

merged

re-enable bisim code, now in domain_theorems.ML

add missing rule to case_strict proof script

remove dead code

domain package no longer generates copy functions; all proofs use take functions instead

need to explicitly include REP_convex

add lemma lub_eq

add lemmas about ssum_map and sprod_map

generate take_take rules

add function define_take_functions

add missing strictify rule to proof script

qualify constructor names with type name

move definition of case combinator to domain_constructors.ML

remove dependence on Domain_Library

more uses of function get_vars

add functions get_vars, get_vars_avoiding

move proofs of pat_rews to domain_constructors.ML

add_domain_constructors takes iso_info record as argument

domain_isomorphism package proves deflation rules for map functions

store deflation thms for map functions in theory data

use function list_ccomb

add function define_const

fix infix declarations

move common functions into new file holcf_library.ML

get rid of incomplete pattern match warnings

move some powerdomain stuff into a new file

move case combinator syntax to domain_constructors.ML

remove redundant code

use correct syntax name for pattern combinator

fix output translation for Case syntax

move definition and syntax of pattern combinators into domain_constructors.ML

domain_isomorphism function returns iso_info record

move proofs of match_rews to domain_constructors.ML

remove dead code

removed dead code

register match functions from domain_constructors.ML

move definition of match combinators to domain_constructors.ML

move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style

move definition of discriminators to domain_constructors.ML

move proofs of when_rews intro domain_constructors.ML

moved proofs of dist_les and dist_eqs to domain_constructors.ML

move proofs of casedist into domain_constructors.ML

move proofs of injects and inverts to domain_constructors.ML

reuse vars_of function

remove unnecessary stuff from argument to add_constructors function

reorder sections

move proof of con_rews into domain_constructor.ML

don't bother returning con_defs

move constructor-specific stuff to a separate function

replace prove_thm function

move proof of compactness rules into domain_constructors.ML

add some convenience functions

rewrite domain package code for selector functions

add function beta_of_def

reorganizing domain package code (in progress)

change domain package's treatment of variable names in theorems to be like datatype package

remove redundant lemma real_minus_half_eq

polished and converted some proofs to Isar style

killed more recdefs

tuned comment

repaired subscripts broken in d8d7d1b785af

repaired definition (cf. d8d7d1b785af)

authentic syntax for *all* logical entities;

mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;

notation for xsymbols (cf. ad039d29e01c);

"_type_prop" is syntax const -- recovered printing of OFCLASS;

removed unused external_names;

cleanup type translations;

adapted to authentic syntax -- actual types are verbatim;

authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;

more systematic mark/unmark operations; tuned;

proper (type_)notation;

proper antiquotations;

standard convention for syntax consts;