2007-07-19 berghofe Replaced "hand-made" files by generated files in Inductive/document.
2007-07-19 berghofe LaTeX code is now generated directly from theory files.
2007-07-19 berghofe LaTeX code is now generated directly from Even and Advanced theories.
2007-07-19 berghofe LaTeX code is now generated directly from theory file.
2007-07-18 aspinall DEEPEN: Use priority message channel for interim messages (not warnings).
2007-07-18 aspinall Direct priority and tracing channels properly.
2007-07-18 paulson tidying using metis
2007-07-17 wenzelm fileident --- produce file identification based;
2007-07-17 wenzelm added ISABELLE_FILE_IDENT (command line for source file identification);
2007-07-17 wenzelm adapted TextIO.inputLine;
2007-07-17 wenzelm tuned comment;
2007-07-17 wenzelm avoid redundant variables in patterns (which made Alice vomit);
2007-07-17 paulson Full sort information by default.
2007-07-17 berghofe Added hypotheses.
2007-07-17 berghofe Added clause for hypotheses to proof_of_xml function.
2007-07-17 wenzelm use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
2007-07-17 krauss reverted fun->recdef, since there are problems with induction rule
2007-07-17 wenzelm Pure theory setup.
2007-07-17 wenzelm Generic print mode.
2007-07-17 wenzelm moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-17 wenzelm simplified loading of ML files -- no static forward references;
2007-07-17 wenzelm moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-07-17 wenzelm added General/print_mode.ML, pure_setup.ML;
2007-07-17 wenzelm tuned specifications;
2007-07-16 krauss use function package
2007-07-16 krauss more proofs
2007-07-16 krauss some interface cleanup
2007-07-16 krauss added lemma binding: accpI = accp.accI
Loading...
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip