2007-07-19 wenzelm 2007-07-19 tuned signature;
2007-07-19 wenzelm 2007-07-19 tuned;
2007-07-19 wenzelm 2007-07-19 replaced info by ident (for full identification, potentially content-based); ident: invoke external lib/scripts/fileident, depending on ISABELLE_FILE_IDENT;
2007-07-19 wenzelm 2007-07-19 added undefined: 'a -> 'b;
2007-07-19 haftmann 2007-07-19 support for SML builtin ints
2007-07-19 haftmann 2007-07-19 adapted to new code generator framework
2007-07-19 haftmann 2007-07-19 code lemma for contents
2007-07-19 haftmann 2007-07-19 code lemma for of_int
2007-07-19 haftmann 2007-07-19 tuned
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories
2007-07-19 haftmann 2007-07-19 added lemmas by Brian Huffman
2007-07-19 haftmann 2007-07-19 moved set Nats to Nat.thy
2007-07-19 haftmann 2007-07-19 added of_int_of_nat
2007-07-19 haftmann 2007-07-19 updated
2007-07-19 berghofe 2007-07-19 strong_ind_simproc now only rewrites arguments of inductive predicates.
2007-07-19 berghofe 2007-07-19 updated
2007-07-19 berghofe 2007-07-19 Refer to major premise of induction rule via "thm_style prem1".
2007-07-19 berghofe 2007-07-19 Added named_thms antiquotation.
2007-07-19 berghofe 2007-07-19 Replaced "hand-made" files by generated files in Inductive/document.
2007-07-19 berghofe 2007-07-19 LaTeX code is now generated directly from theory files.
2007-07-19 berghofe 2007-07-19 LaTeX code is now generated directly from Even and Advanced theories.
2007-07-19 berghofe 2007-07-19 LaTeX code is now generated directly from theory file.
2007-07-18 aspinall 2007-07-18 DEEPEN: Use priority message channel for interim messages (not warnings).
2007-07-18 aspinall 2007-07-18 Direct priority and tracing channels properly.
2007-07-18 paulson 2007-07-18 tidying using metis
2007-07-17 wenzelm 2007-07-17 fileident --- produce file identification based;
2007-07-17 wenzelm 2007-07-17 added ISABELLE_FILE_IDENT (command line for source file identification);
2007-07-17 wenzelm 2007-07-17 adapted TextIO.inputLine;
2007-07-17 wenzelm 2007-07-17 tuned comment;
2007-07-17 wenzelm 2007-07-17 avoid redundant variables in patterns (which made Alice vomit);
2007-07-17 paulson 2007-07-17 Full sort information by default. Race condition on successful proofs fixed.
2007-07-17 berghofe 2007-07-17 Added hypotheses.
2007-07-17 berghofe 2007-07-17 Added clause for hypotheses to proof_of_xml function.
2007-07-17 wenzelm 2007-07-17 use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
2007-07-17 krauss 2007-07-17 reverted fun->recdef, since there are problems with induction rule
2007-07-17 wenzelm 2007-07-17 Pure theory setup.
2007-07-17 wenzelm 2007-07-17 Generic print mode.
2007-07-17 wenzelm 2007-07-17 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-17 wenzelm 2007-07-17 simplified loading of ML files -- no static forward references;
2007-07-17 wenzelm 2007-07-17 moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-07-17 wenzelm 2007-07-17 added General/print_mode.ML, pure_setup.ML;
2007-07-17 wenzelm 2007-07-17 tuned specifications;
2007-07-16 krauss 2007-07-16 use function package
2007-07-16 krauss 2007-07-16 more proofs
2007-07-16 krauss 2007-07-16 some interface cleanup
2007-07-16 krauss 2007-07-16 added lemma binding: accpI = accp.accI
2007-07-16 krauss 2007-07-16 updated
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 paulson 2007-07-16 tidied
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
2007-07-16 haftmann 2007-07-16 clarified structure names
2007-07-16 haftmann 2007-07-16 added function for case certificates
2007-07-16 haftmann 2007-07-16 dropped outer ROOT structure for generated code
2007-07-16 haftmann 2007-07-16 tuned
2007-07-16 haftmann 2007-07-16 fixed SML/NJ int problem
2007-07-16 haftmann 2007-07-16 updated
2007-07-13 wenzelm 2007-07-13 tuned;
2007-07-12 krauss 2007-07-12 updated
2007-07-12 wenzelm 2007-07-12 updated;