record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);

record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);

eliminated Args.bang_facts (legacy feature);

eliminated old-style prems; tuned proofs;

removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);

Some notes on platform support of Isabelle.

"private" map_of_map lemma

added insort_insert

added dom_option_map, map_of_map_keys

added bulkload; tuned document

merged

merged

moved lemma map_sorted_distinct_set_unique

various refinements

print message when finiteness of domain definition is detected

merged

skip coinduction proofs for indirect-recursive domain definitions

merged

introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'

add comment

move take_proofs-related stuff to a new section

remove dead code

tuned dead code;

use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;

merged

fix proof script so 'domain foo = Foo foo' works

fix proof script so qdomain_isomorphism foo = foo' works

finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;

isabelle browser -b: Admin/build only;

merged

skip proof of induction rule for indirect-recursive domain definitions

generalized inj_uminus; added strict_mono_imp_inj_on

merged

Add Lebesgue integral and probability space.

Supremum and Infimum on real intervals

Rewrite rules for images of minus of intervals

Add dense_le, dense_le_bounded, field_le_mult_one_interval.

Added natfloor and floor rules for multiplication and power.

Generalized setsum_cases

Added vimage_inter_cong

merged

move coinduction-related stuff into function prove_coindunction

add function add_qualified_simp_thm

generate lemma take_below, declare chain_take [simp]

switch to polyml-svn;

basic simplification of external_prover signature;

tuned;

renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort; metis: type_has_topsort leads to tactic failure (with warning), like other metis failures;

point to http://hginit.com/

Simplified a couple of proofs and corrected a comment

lemmas set_map_of_compr, map_of_inject_set

merged

merged

remove dead code

add infix declarations

remove unnecessary theorem references

remove copy_of_dtyp from domain_axioms.ML

add_axioms returns an iso_info; add_theorems takes an iso_info as an argument

uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate

add function axiomatize_lub_take

move function mk_lub into holcf_library.ML

added extern_syntax;

merged

more uniform naming conventions

tuned whitespace

restructured RBT theory

stats for at-poly-test;

proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);

merged, resolving some basic conflicts;

merged

updated patch for hgweb style: now applies to Mercurial 1.4.3 templates

fix fragile proof using old induction rule (cf. bdf8ad377877)

merged

replaced \<bullet> with inner

tuned

the ordering on real^1 is linear

merged

made smlnj happy

adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck

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