2005-10-17 berghofe 2005-10-17 Improved proof of injectivity theorems to make it work on "ordinary" function types as well.
2005-10-17 berghofe 2005-10-17 Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17 berghofe 2005-10-17 Implemented proofs for support and freshness theorems.
2005-10-17 urbanc 2005-10-17 deleted leading space in the definition of fresh
2005-10-17 berghofe 2005-10-17 Initial revision.
2005-10-15 wenzelm 2005-10-15 tuned;
2005-10-15 wenzelm 2005-10-15 tuned comment;
2005-10-15 wenzelm 2005-10-15 added ML_type, ML_struct;
2005-10-15 wenzelm 2005-10-15 more;
2005-10-15 wenzelm 2005-10-15 * antiquotations ML_type, ML_struct; * Isar 'guess' element;
2005-10-15 wenzelm 2005-10-15 added guess;
2005-10-15 wenzelm 2005-10-15 added antiquotations ML_type, ML_struct;
2005-10-15 wenzelm 2005-10-15 use perl for test/stat;
2005-10-15 wenzelm 2005-10-15 export strip_params;
2005-10-15 wenzelm 2005-10-15 note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;
2005-10-15 wenzelm 2005-10-15 goal statements: before_qed argument;
2005-10-15 wenzelm 2005-10-15 added 'guess', which derives the obtained context from the course of reasoning;
2005-10-15 wenzelm 2005-10-15 added primitive_text, succeed_text;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument;
2005-10-15 wenzelm 2005-10-15 added 'guess';
2005-10-15 wenzelm 2005-10-15 tuned;
2005-10-15 wenzelm 2005-10-15 added no_facts;
2005-10-15 wenzelm 2005-10-15 tuned comments;
2005-10-15 wenzelm 2005-10-15 updated;
2005-10-14 paulson 2005-10-14 signature changes
2005-10-14 haftmann 2005-10-14 added module rat.ML for rational numbers
2005-10-14 isatest 2005-10-14 longer time out for test (kleing)
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-13 wenzelm 2005-10-13 obsolete;
2005-10-12 webertj 2005-10-12 counter added to SAT signature
2005-10-12 webertj 2005-10-12 no proof reconstruction when quick_and_dirty is set
2005-10-12 paulson 2005-10-12 tidying
2005-10-12 huffman 2005-10-12 domain package generates compactness lemmas for new constructors
2005-10-12 huffman 2005-10-12 add ML bindings for compactness lemmas
2005-10-12 huffman 2005-10-12 added compactness theorems
2005-10-12 huffman 2005-10-12 added compactness lemmas; cleaned up
2005-10-11 huffman 2005-10-11 added compactness theorems in locale iso
2005-10-11 huffman 2005-10-11 added several theorems in locale iso
2005-10-11 huffman 2005-10-11 added xsymbols syntax for pairs; cleaned up
2005-10-11 huffman 2005-10-11 added theorem typedef_compact
2005-10-11 huffman 2005-10-11 rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
2005-10-11 huffman 2005-10-11 cleaned up; renamed less_fun to expand_fun_less
2005-10-11 nipkow 2005-10-11 added hd lemma
2005-10-11 paulson 2005-10-11 simplifying the treatment of clausification
2005-10-11 paulson 2005-10-11 simplifying the treatment of nameless theorems
2005-10-11 wenzelm 2005-10-11 expand: error on undefined/empty env variable; tuned;
2005-10-11 wenzelm 2005-10-11 added assert; tuned;
2005-10-11 wenzelm 2005-10-11 tuned;
2005-10-11 wenzelm 2005-10-11 added string_of_pid;
2005-10-11 wenzelm 2005-10-11 raw symbols: allow non-ASCII chars (e.g. UTF-8); tuned comment;
2005-10-11 wenzelm 2005-10-11 moved string_of_pid to ML-Systems;
2005-10-11 wenzelm 2005-10-11 ML_SUFFIX in targets (experimental);
2005-10-11 wenzelm 2005-10-11 cleanup backup images;
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-10-10 wenzelm 2005-10-10 updated print_tac;
2005-10-10 huffman 2005-10-10 add names to infix declarations
2005-10-10 huffman 2005-10-10 new syntax translations for continuous lambda abstraction
2005-10-10 huffman 2005-10-10 removed Istrictify; simplified some proofs