2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-29 wenzelm 2010-12-29 check_file: secondary load path is legacy feature;
2010-12-29 wenzelm 2010-12-29 share_common_data dummy;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-29 wenzelm 2010-12-29 tuned comments;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy; more accurate dependencies;
2010-12-28 wenzelm 2010-12-28 made SML/NJ happy;
2010-12-27 krauss 2010-12-27 function (tailrec) is a legacy feature
2010-12-25 krauss 2010-12-25 dropped duplicate unused lemmas; spelling
2010-12-25 krauss 2010-12-25 partial_function (tailrec) replaces function (tailrec); dropped unnecessary domain reasoning; curried polydivide_aux
2010-12-24 huffman 2010-12-24 remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
2010-12-23 huffman 2010-12-23 NEWS updates for HOLCF
2010-12-23 huffman 2010-12-23 replaced separate lemmas seq{1,2,3} with seq_simps
2010-12-23 huffman 2010-12-23 changed syntax of powerdomain binary union operators
2010-12-23 haftmann 2010-12-23 tuned order of NEWS
2010-12-23 haftmann 2010-12-23 NEWS
2010-12-23 haftmann 2010-12-23 documentation stub on type_lifting
2010-12-23 haftmann 2010-12-23 tuned comments and line breaks
2010-12-22 huffman 2010-12-22 rename function ideal_completion.basis_fun to ideal_completion.extension
2010-12-22 huffman 2010-12-22 fix another proof script broken by a35af5180c01
2010-12-22 huffman 2010-12-22 fix proof script broken by a35af5180c01
2010-12-22 haftmann 2010-12-22 merged
2010-12-22 haftmann 2010-12-22 full localization with possibly multiple entries; explicit prohibition of fixed type variables
2010-12-22 haftmann 2010-12-22 tool-compliant mapper declaration
2010-12-22 haftmann 2010-12-22 more proof contexts; formal declaration
2010-12-22 haftmann 2010-12-22 mapper is arbitrary term, not only constant; proper backward proofs of derived properties
2010-12-22 haftmann 2010-12-22 tuned comment
2010-12-22 wenzelm 2010-12-22 merged
2010-12-22 blanchet 2010-12-22 made SML/NJ happy
2010-12-22 wenzelm 2010-12-22 check JVM later, to avoid potential conflict with jEdit splash screen;
2010-12-22 wenzelm 2010-12-22 explicit JVM check on startup;
2010-12-22 wenzelm 2010-12-22 more explicit jvm_name;
2010-12-22 wenzelm 2010-12-22 isabelle java: prefer -server here;
2010-12-21 wenzelm 2010-12-21 configuration option "rule_trace"; discontinued preference "trace-rules";
2010-12-21 wenzelm 2010-12-21 configuration option "syntax_branching_level";
2010-12-21 wenzelm 2010-12-21 configuration option "syntax_ast_trace" and "syntax_ast_stat";
2010-12-21 wenzelm 2010-12-21 more robust ML antiquotations -- allow original tokens without adjacent whitespace;
2010-12-21 wenzelm 2010-12-21 configuration option "ML_trace";
2010-12-21 haftmann 2010-12-21 merged
2010-12-21 haftmann 2010-12-21 id_const replaces mk_id
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-21 haftmann 2010-12-21 prove more algebraic version of functorial properties; retain old properties for convenience
2010-12-21 huffman 2010-12-21 declare more simp rules, rewrite proofs in Isar-style
2010-12-21 hoelzl 2010-12-21 merged
2010-12-21 hoelzl 2010-12-21 use DERIV_intros
2010-12-21 hoelzl 2010-12-21 generalized monoseq, decseq and incseq; simplified proof for seq_monosub
2010-12-21 haftmann 2010-12-21 merged
2010-12-21 haftmann 2010-12-21 proper static closures
2010-12-21 haftmann 2010-12-21 tuned names
2010-12-21 haftmann 2010-12-21 renamed mk_id to the more canonical id_const
2010-12-21 blanchet 2010-12-21 merged
2010-12-21 blanchet 2010-12-21 better parsing of options, in case the value has '='
2010-12-21 blanchet 2010-12-21 show the relation
2010-12-21 blanchet 2010-12-21 merged
2010-12-21 blanchet 2010-12-21 renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy"
2010-12-21 blanchet 2010-12-21 added "sledgehammer_tac" as possible reconstructor in Mirabelle
2010-12-21 wenzelm 2010-12-21 merged
2010-12-21 boehmes 2010-12-21 merged
2010-12-21 boehmes 2010-12-21 also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)