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;

more precise scope of exception handler;

eliminated hard tabs;

tuned final whitespace;

repaired 'definition' (cf. d8d7d1b785af);

merged

more recdef (and old primrec) hunting

killed recdefs in HOL-Auth

merged

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

export add_quotient_type.

updated generated files;

added type_notation command;

more uniform treatment of syntax for types vs. consts;

made smlnj happy

more antiquotations;

more antiquotations; eliminated legacy ML bindings;

modernized structure Term_Ord;

use existing Typ_Graph;

further standard instances of functor Graph;

code simplification by inlining;

just one copy of structure Term_Graph (in Pure);

modernized structure Int_Graph;

clarified @{const_name} vs. @{const_abbrev};

clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;

type/const name: explicitly allow abbreviations as well;

clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;