2008-10-21 wenzelm less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21 wenzelm JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21 wenzelm make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21 berghofe Added nominal_inductive2.
2008-10-21 berghofe Example for using the generalized version of nominal_inductive.
2008-10-21 berghofe Added theory W.
2008-10-21 berghofe More general, still experimental version of nominal_inductive for
2008-10-21 berghofe Added nominal_inductive2.ML
2008-10-21 wenzelm added jEdit settings;
2008-10-21 wenzelm tuned usage line;
2008-10-21 wenzelm Isabelle/jEdit interface wrapper.
2008-10-21 wenzelm join results in isolation;
2008-10-21 wenzelm join_results: allow CRITICAL join of finished futures;
2008-10-21 wenzelm Future.join_result;
2008-10-21 wenzelm added Future.enabled check;
2008-10-21 wenzelm ThyOutput: export some auxiliary operations;
2008-10-20 nipkow fixed proof
2008-10-20 nipkow added lemmas
2008-10-19 berghofe Names of variables in perm_eqs are now chosen more carefully to avoid
2008-10-19 berghofe - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-19 berghofe datatype_codegen now checks name of result type of constructor
2008-10-19 wenzelm run a program in a modified environment;
2008-10-17 wenzelm reactivated HOL-Matrix;
2008-10-17 haftmann tuned
2008-10-17 haftmann filled remaining gaps
2008-10-17 haftmann added type antiquotation
2008-10-16 wenzelm tuned;
2008-10-16 wenzelm added dep for Concurrent/ROOT.ML;
2008-10-16 wenzelm tuned;
2008-10-16 wenzelm removed Locales;
2008-10-16 wenzelm goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16 wenzelm added translations for SORT_CONSTRAINT
2008-10-16 wenzelm conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16 wenzelm added make;
2008-10-16 wenzelm maintain sort occurrences of declared terms;
2008-10-16 wenzelm added weaken_sorts;
2008-10-16 wenzelm added make, minimal_sorts;
2008-10-16 wenzelm added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16 wenzelm added check_shyps, which reject pending sort hypotheses;
2008-10-16 wenzelm Drule.norm_hhf_eqs;
2008-10-16 wenzelm prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16 wenzelm added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16 wenzelm tuned;
2008-10-16 wenzelm avoid accidental dependency of automated proof on sort equiv;
2008-10-16 wenzelm explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16 wenzelm avoid CRITICAL with_path;
2008-10-16 huffman rewrite more proofs in Isar style
2008-10-16 ballarin Removed ex/Locales.thy.
2008-10-16 ballarin More occurrences of 'includes' gone.
2008-10-16 ballarin Removed outdated locales tutorial.
2008-10-16 haftmann correct rounding
2008-10-16 haftmann circumvent some TeX problem
2008-10-15 kleing only test HOL image for smlnj
2008-10-15 wenzelm tuned;
2008-10-15 wenzelm tuned;
2008-10-15 wenzelm generic ATP manager based on threads (by Fabian Immler);
2008-10-15 wenzelm added sledgehammer etc.;
2008-10-15 wenzelm removed obsolete Complex sessions;
2008-10-15 haftmann figure for adaption
2008-10-15 ballarin Removed 'includes' (fixed).
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip