more work on Nitpick's finite sets

improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"

ProofContext.read_class/read_type_name_proper;

added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;

simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;

tuned -- eliminated Sign.intern_sort;

renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;

added "finitize" option to Nitpick + remove dependency on "Coinductive_List"

merged

remove unnecessary error handling code

construct fully typed goal in proof of induction rule

don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule

remove redundant function arguments

include take_info within take_induct_info type

pass take_info as an argument to comp_theorems

pass take_induct_info as an argument to comp_theorems

add type take_induct_info

generate take_induct lemmas

move proofs of reach and take lemmas to domain_take_proofs.ML

move lemmas from Domain.thy to Domain_Aux.thy

move take-proofs stuff into new theory Domain_Aux.thy

add type take_info

add function add_qualified_def

merged

proper ML interface; further polishing

code simplification and tuning

Added inducts field to inductive_result.

transfer: avoid camel case, more standard coding conventions, misc tuning

transfer: avoid camel case

merged

generate separate qualified theorem name for each type's reach and take_lemma

add simp rule LAM_strict

fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'

merged

dropped dead code; adhere more closely to standard coding conventions

merged

arith tactic uses 'priority' instead of 'warning' to print messages

add simp rules about Ints, Nats

add more simp rules for Ints

add lemmas Nats_cases and Nats_induct

generalize some lemmas, and remove a few unnecessary ones

generalize some lemmas from class linordered_ring_strict to linordered_ring

add case_names attribute to casedist and ind rules

add some lemmas about complete lattices

Digesting strings according to SHA-1.

proper int wrapping for Word32;

separate structure Typedecl;

modernized structure Object_Logic;

modernized structure Local_Defs;

merged

merged

simplified

merged

lemma restrict_complement_singleton_eq

some lemma refinements

added Table.thy

provide ProofContext.def_type depending on "pattern" mode;

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