2006-12-29 wenzelm 2006-12-29 removed obsolete init_pgip; removed obsolete redo, context_thy etc.;
2006-12-29 wenzelm 2006-12-29 removed obsolete init_context;
2006-12-29 wenzelm 2006-12-29 obsolete (cf. ProofGeneral/proof_general_emacs.ML);
2006-12-29 wenzelm 2006-12-29 tuned;
2006-12-29 wenzelm 2006-12-29 signed_string_of_int;
2006-12-29 wenzelm 2006-12-29 added proper header;
2006-12-29 wenzelm 2006-12-29 added signed_string_of_int (pruduces proper - instead of SML's ~);
2006-12-29 wenzelm 2006-12-29 removed obsolete proof_general.ML;
2006-12-29 wenzelm 2006-12-29 minor tuning;
2006-12-29 wenzelm 2006-12-29 tuned specifications/proofs;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;
2006-12-29 wenzelm 2006-12-29 renamed Graph.project to Graph.subgraph;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;
2006-12-29 wenzelm 2006-12-29 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
2006-12-29 wenzelm 2006-12-29 Sorts.minimal_classes;
2006-12-29 wenzelm 2006-12-29 classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;
2006-12-29 wenzelm 2006-12-29 replaced classes by all_classes (topologically sorted); added minimal_classes;
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29 aspinall 2006-12-29 Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
2006-12-29 aspinall 2006-12-29 Typo in last commit
2006-12-29 haftmann 2006-12-29 explicit construction of operational classes
2006-12-29 haftmann 2006-12-29 added handling for explicit classrel witnesses
2006-12-29 haftmann 2006-12-29 ``classes`` now returns classes in topological order
2006-12-29 haftmann 2006-12-29 dropped some bookkeeping
2006-12-29 haftmann 2006-12-29 simplified class_package
2006-12-29 wenzelm 2006-12-29 use_ml: reverted to simple output (Poly/ML changed);
2006-12-28 haftmann 2006-12-28 removed private files
2006-12-28 wenzelm 2006-12-28 tuned;
2006-12-28 wenzelm 2006-12-28 removed nospaces (Char.isSpace does not conform to Isabelle conventions);
2006-12-28 wenzelm 2006-12-28 tuned msg;
2006-12-28 wenzelm 2006-12-28 inlined nospaces (from library.ML);
2006-12-28 haftmann 2006-12-28 added
2006-12-27 haftmann 2006-12-27 some clarifications
2006-12-27 haftmann 2006-12-27 different handling of type variable names
2006-12-27 haftmann 2006-12-27 added split
2006-12-27 haftmann 2006-12-27 fixed misleading error message
2006-12-27 haftmann 2006-12-27 dropped section header
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-12-27 haftmann 2006-12-27 removed Haskell reserved words
2006-12-27 haftmann 2006-12-27 removed Main.thy
2006-12-27 haftmann 2006-12-27 moved code generator product setup here
2006-12-27 haftmann 2006-12-27 added code generator test theory
2006-12-27 haftmann 2006-12-27 explizit serialization for Haskell id
2006-12-27 haftmann 2006-12-27 removed code generation stuff belonging to other theories
2006-12-27 haftmann 2006-12-27 moved code generator bool setup here
2006-12-27 haftmann 2006-12-27 exported explicit equality on tokens
2006-12-27 haftmann 2006-12-27 made SML/NJ happy
2006-12-22 paulson 2006-12-22 revised for new make_clauses
2006-12-22 paulson 2006-12-22 tidying the ATP communications
2006-12-22 paulson 2006-12-22 string primtives
2006-12-22 haftmann 2006-12-22 deactivated test for the moment
2006-12-22 paulson 2006-12-22 fixed typo in comment
2006-12-22 ballarin 2006-12-22 Experimenting with interpretations of "definition".
2006-12-21 haftmann 2006-12-21 clarified code
2006-12-21 haftmann 2006-12-21 dropped superfluos code
2006-12-21 haftmann 2006-12-21 code clarifications
2006-12-21 haftmann 2006-12-21 import path made absolute
2006-12-21 haftmann 2006-12-21 added code lemmas for quantification over bounded nats
2006-12-21 aspinall 2006-12-21 Disable new Proof General code until SML/NJ compile fixed.
2006-12-20 aspinall 2006-12-20 Use new Proof General code by default [see comment for reverting]