2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-06-11 wenzelm 2005-06-11 renamed Sign.intern_tycon to Sign.intern_type;
2005-06-11 wenzelm 2005-06-11 fixed spelling;
2005-06-11 obua 2005-06-11 further optimizations of cycle test
2005-06-10 nipkow 2005-06-10 tuned
2005-06-10 nipkow 2005-06-10 tuning
2005-06-10 nipkow 2005-06-10 IntInf change
2005-06-10 quigley 2005-06-10 All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG.
2005-06-09 wenzelm 2005-06-09 added Isar_examples/Drinker.thy;
2005-06-09 wenzelm 2005-06-09 full Display.pprint_theory for ML toplevel facilitates debugging;
2005-06-09 wenzelm 2005-06-09 simplified is_stale, check_stale; fixed map_sg -- proper treatment of non-drafts;
2005-06-09 wenzelm 2005-06-09 updated;
2005-06-09 wenzelm 2005-06-09 axioms: NameSpace.table;
2005-06-09 wenzelm 2005-06-09 PureThy.all_thms_of;
2005-06-09 wenzelm 2005-06-09 Theory.all_axioms_of, PureThy.all_thms_of;
2005-06-09 wenzelm 2005-06-09 can (Thm.get_axiom_i thy) name; removed duplicate code;
2005-06-09 wenzelm 2005-06-09 renamed extern to extern_thm; renamed cert/read_typ_raw to cert/read_typ_abbrev; added cert/read_typ_syntax; thms: NameSpace.table;
2005-06-09 wenzelm 2005-06-09 meths: NameSpace.table;
2005-06-09 wenzelm 2005-06-09 NameSpace.extern_table; ProofContext.extern_thm;
2005-06-09 wenzelm 2005-06-09 Args.local_typ_abbrev;
2005-06-09 wenzelm 2005-06-09 attribs: NameSpace.table;
2005-06-09 wenzelm 2005-06-09 renamed global/local_typ_raw to global/local_typ_abbrev;
2005-06-09 wenzelm 2005-06-09 added structure Inttab; tuned comments;
2005-06-09 wenzelm 2005-06-09 added type NameSpace.table with basic operations;
2005-06-09 wenzelm 2005-06-09 renamed cert_typ_raw to cert_typ_abbrev; renamed add_abbrs to add_abbrevs; tuned;
2005-06-09 wenzelm 2005-06-09 axioms and oracles: NameSpace.table; added axioms_of, all_axioms_of;
2005-06-09 wenzelm 2005-06-09 map_typ and map_term no longer global;
2005-06-09 wenzelm 2005-06-09 Major cleanup: got rid of types bclass, xclass, xsort, xtyp, xterm; reorganized code to separate stamps/data/sign; clarified name space inter/extern operations; sane read/certify operations -- more picky about stale signatures; sane implementation of signature extensions;
2005-06-09 wenzelm 2005-06-09 thms_of no longer global; added all_thms_of; theorems: NameSpace.table;
2005-06-09 wenzelm 2005-06-09 NameSpace.extern_table;
2005-06-09 wenzelm 2005-06-09 print_theory: omit name spaces; NameSpace.extern_table;
2005-06-09 wenzelm 2005-06-09 got rid of bclass, xclass;
2005-06-09 wenzelm 2005-06-09 add_axioms_infer -- avoids use of stale theory;
2005-06-09 wenzelm 2005-06-09 Theory.all_axioms_of;
2005-06-09 wenzelm 2005-06-09 Sign.read_typ_abbrev;
2005-06-09 haftmann 2005-06-09 added chmod for packages
2005-06-09 haftmann 2005-06-09 added CONTRIBUTORS
2005-06-09 haftmann 2005-06-09 a very little cleanup
2005-06-08 huffman 2005-06-08 make up_eq and up_less into simp rules
2005-06-08 ballarin 2005-06-08 Fixed "axiom" generation for mixed locales with and without predicates.
2005-06-08 haftmann 2005-06-08 added some notes
2005-06-08 haftmann 2005-06-08 added file acces rights handling
2005-06-08 huffman 2005-06-08 fix usage of inverts lemma, which has fewer premises now
2005-06-08 huffman 2005-06-08 faster proofs of inverts and injects lemmas, with fewer strictness hypotheses
2005-06-08 huffman 2005-06-08 fixed renamed lemma
2005-06-08 huffman 2005-06-08 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
2005-06-08 huffman 2005-06-08 added theorems is_ub_range_shift and is_lub_range_shift
2005-06-08 huffman 2005-06-08 added theorems less_sprod, spair_less, spair_eq, spair_inject
2005-06-08 huffman 2005-06-08 renamed theorems less_ssum4a,b,c,d to more meaningful names
2005-06-08 huffman 2005-06-08 added theorem less_cprod
2005-06-08 huffman 2005-06-08 added theorem injection_less
2005-06-07 obua 2005-06-07 A flag DEFS_CHAIN_HISTORY can be used to improve the error message in case a cycle has been detected. If it is switched off and a cycle has been detected, the user is notified that there is such a flag.
2005-06-07 haftmann 2005-06-07 extended readme
2005-06-07 haftmann 2005-06-07 started migration framwork script
2005-06-07 haftmann 2005-06-07 added basics for generic migration tool
2005-06-07 haftmann 2005-06-07 added isatest-lint prototype
2005-06-07 obua 2005-06-07 1) Fixed bug in Defs.merge_edges_1. 2) Major optimization of Defs.define: do not store dependencies between constants that cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to theories that define their constants in HOL-light / HOL4 style. 3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
2005-06-06 nipkow 2005-06-06 *** empty log message ***
2005-06-06 nipkow 2005-06-06 updating...
2005-06-06 nipkow 2005-06-06 Added the t = x "fix" - in (* ... *) :-(