2006-09-05 ago wenzelm tuned;
2006-09-05 ago wenzelm more on names;
2006-09-04 ago wenzelm tuned;
2006-09-04 ago wenzelm tuned;
2006-09-04 ago paulson Using Drule.local_standard to reduce the space usage
2006-09-04 ago wenzelm tuned;
2006-09-04 ago wenzelm updated;
2006-09-04 ago wenzelm more on variables;
2006-09-04 ago ballarin More locale test code.
2006-09-04 ago ballarin Documented methods intro_locales and unfold_locales.
2006-09-04 ago haftmann some corrections in class section
2006-09-04 ago haftmann explicit table with constant types
2006-09-04 ago haftmann proper project_sort
2006-09-02 ago webertj tuned
2006-09-02 ago webertj zchaff_with_proofs: proof is a reference now
2006-09-01 ago wenzelm signature: do not export private stuff;
2006-09-01 ago wenzelm skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
2006-09-01 ago wenzelm tuned;
2006-09-01 ago wenzelm tuned;
2006-09-01 ago wenzelm explain assumptions;
2006-09-01 ago paulson refinements to conversion into clause form, esp for the HO case
2006-09-01 ago haftmann pervasive refinements
2006-09-01 ago haftmann removed some dictionary stuff
2006-09-01 ago haftmann project_algebra yields sort projector
2006-09-01 ago haftmann final syntax for some Isar code generator keywords
2006-08-31 ago wenzelm tuned;
2006-08-31 ago wenzelm misc cleanup;
2006-08-31 ago wenzelm tuned;
2006-08-31 ago wenzelm more stuff;
2006-08-31 ago wenzelm mldecls: footnotesize;
2006-08-31 ago wenzelm more on contexts;
2006-08-31 ago webertj String.concatWith (not available in PolyML) replaced by space_implode
2006-08-31 ago paulson improvements to abstraction generation
2006-08-31 ago paulson blacklist now handles thm lists
2006-08-31 ago paulson Empty is better than Match
2006-08-31 ago webertj term_of_prop_formula added
2006-08-31 ago webertj read_dimacs_cnf_file ignores more comment lines
2006-08-30 ago webertj faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-08-30 ago haftmann code refinements
2006-08-30 ago wenzelm updated;
2006-08-30 ago wenzelm tuned;
2006-08-30 ago haftmann added yet another code generator example
2006-08-30 ago haftmann fixes
2006-08-30 ago haftmann fixed bug in wfrec appgen
2006-08-30 ago webertj lin_arith_prover: splitting reverted because of performance loss
2006-08-30 ago webertj lin_arith_prover: splitting reverted because of performance loss
2006-08-29 ago urbanc added a FIXME-comment
2006-08-29 ago wenzelm tuned;
2006-08-29 ago wenzelm more on contexts;
2006-08-29 ago haftmann refinements
2006-08-29 ago haftmann added and refined some exmples
2006-08-29 ago haftmann added typecopy_package
2006-08-29 ago haftmann added typecopy_package and some examples
2006-08-29 ago haftmann updated keywords
2006-08-28 ago paulson minor bug fixes
2006-08-28 ago paulson removed the (apparently pointless) signature constraint
2006-08-28 ago paulson tidied
2006-08-28 ago webertj encode clauses as Isar premises, rather than as object-logic &, for faster parsing
2006-08-25 ago paulson abstraction of lambda-expressions
2006-08-25 ago paulson tidied