2010-03-06 haftmann 2010-03-06 lemma restrict_complement_singleton_eq
2010-03-06 haftmann 2010-03-06 some lemma refinements
2010-03-06 haftmann 2010-03-06 added Table.thy
2010-03-06 wenzelm 2010-03-06 provide ProofContext.def_type depending on "pattern" mode;
2010-03-06 wenzelm 2010-03-06 record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
2010-03-06 wenzelm 2010-03-06 record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-03-06 wenzelm 2010-03-06 eliminated old-style prems; tuned proofs;
2010-03-06 wenzelm 2010-03-06 removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
2010-03-06 wenzelm 2010-03-06 Some notes on platform support of Isabelle.
2010-03-06 haftmann 2010-03-06 "private" map_of_map lemma
2010-03-06 haftmann 2010-03-06 added insort_insert
2010-03-06 haftmann 2010-03-06 added dom_option_map, map_of_map_keys
2010-03-06 haftmann 2010-03-06 added bulkload; tuned document
2010-03-06 haftmann 2010-03-06 merged
2010-03-05 haftmann 2010-03-05 merged
2010-03-05 haftmann 2010-03-05 moved lemma map_sorted_distinct_set_unique
2010-03-05 haftmann 2010-03-05 various refinements
2010-03-05 huffman 2010-03-05 print message when finiteness of domain definition is detected
2010-03-05 huffman 2010-03-05 merged
2010-03-05 huffman 2010-03-05 skip coinduction proofs for indirect-recursive domain definitions
2010-03-06 wenzelm 2010-03-06 merged
2010-03-05 huffman 2010-03-05 introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
2010-03-05 huffman 2010-03-05 add comment
2010-03-05 huffman 2010-03-05 move take_proofs-related stuff to a new section
2010-03-05 huffman 2010-03-05 remove dead code
2010-03-05 wenzelm 2010-03-05 tuned dead code;
2010-03-05 wenzelm 2010-03-05 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
2010-03-05 wenzelm 2010-03-05 merged
2010-03-05 huffman 2010-03-05 fix proof script so 'domain foo = Foo foo' works
2010-03-05 huffman 2010-03-05 fix proof script so qdomain_isomorphism foo = foo' works
2010-03-05 wenzelm 2010-03-05 finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
2010-03-05 wenzelm 2010-03-05 isabelle browser -b: Admin/build only;
2010-03-05 huffman 2010-03-05 merged
2010-03-05 huffman 2010-03-05 skip proof of induction rule for indirect-recursive domain definitions
2010-03-05 hoelzl 2010-03-05 generalized inj_uminus; added strict_mono_imp_inj_on
2010-03-05 hoelzl 2010-03-05 merged
2010-03-04 hoelzl 2010-03-04 Add Lebesgue integral and probability space.
2010-03-04 hoelzl 2010-03-04 Supremum and Infimum on real intervals
2010-03-04 hoelzl 2010-03-04 Rewrite rules for images of minus of intervals
2010-03-04 hoelzl 2010-03-04 Add dense_le, dense_le_bounded, field_le_mult_one_interval.
2010-03-04 hoelzl 2010-03-04 Added natfloor and floor rules for multiplication and power.
2010-03-04 hoelzl 2010-03-04 Generalized setsum_cases
2010-03-04 hoelzl 2010-03-04 Added vimage_inter_cong
2010-03-04 huffman 2010-03-04 merged
2010-03-04 huffman 2010-03-04 move coinduction-related stuff into function prove_coindunction
2010-03-04 huffman 2010-03-04 add function add_qualified_simp_thm
2010-03-03 huffman 2010-03-03 generate lemma take_below, declare chain_take [simp]
2010-03-04 wenzelm 2010-03-04 switch to polyml-svn;
2010-03-04 wenzelm 2010-03-04 basic simplification of external_prover signature;
2010-03-04 wenzelm 2010-03-04 tuned;
2010-03-04 wenzelm 2010-03-04 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;
2010-03-04 wenzelm 2010-03-04 point to http://hginit.com/
2010-03-04 paulson 2010-03-04 Simplified a couple of proofs and corrected a comment
2010-03-04 haftmann 2010-03-04 lemmas set_map_of_compr, map_of_inject_set
2010-03-03 huffman 2010-03-03 merged
2010-03-03 huffman 2010-03-03 merged
2010-03-03 huffman 2010-03-03 remove dead code
2010-03-03 huffman 2010-03-03 add infix declarations
2010-03-03 huffman 2010-03-03 remove unnecessary theorem references