2005-06-17 wenzelm 2005-06-17 RuleCases.tactic; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; tuned;
2005-06-17 wenzelm 2005-06-17 (RAW_)METHOD_CASES: RuleCases.tactic; accomodate change of TheoryDataFun;
2005-06-17 wenzelm 2005-06-17 Theory.add_typedecls; Sign.local_path;
2005-06-17 wenzelm 2005-06-17 added map', fold; changed join to pass key;
2005-06-17 wenzelm 2005-06-17 Table.fold;
2005-06-17 wenzelm 2005-06-17 Symtab.fold;
2005-06-17 wenzelm 2005-06-17 type theory, theory_ref, exception THEORY and related operations imported from Context; actual theory content declared as theory data; removed syn_of; import theory operations in SIGN_THEORY from Sign; tuned;
2005-06-17 wenzelm 2005-06-17 obsolete type sg is now an alias for Context.theory; code and interfaces related to stamps and data now in context.ML; actual signature content declared as theory data; removed type sg_ref (superceded by theory_ref); signature SIGN_THEORY lists theory operations that are duplicated in Theory;
2005-06-17 wenzelm 2005-06-17 added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;
2005-06-17 wenzelm 2005-06-17 Context.theory_name; tuned;
2005-06-17 wenzelm 2005-06-17 added serial numbers;
2005-06-17 wenzelm 2005-06-17 removed obsolete pretty printers for Theory.theory, Sign.sg; added pretty printer for Context.theory (long form of output);
2005-06-17 wenzelm 2005-06-17 removed pretty_theory, pprint_theory (see context.ML or thy_info.ML); removed obsolete pretty_name_space; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 added type theory: generic theory contexts with unique identity, arbitrarily typed data, linear and graph development -- a complete rewrite of code that used to be spread over in sign.ML, theory.ML, theory_data.ML, pure_thy.ML;
2005-06-17 wenzelm 2005-06-17 removed Pure/theory_data.ML;
2005-06-17 wenzelm 2005-06-17 added Id;
2005-06-17 wenzelm 2005-06-17 Theory.merge;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Context.theory_name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Sign.the_const_type; Context.exists_name;
2005-06-17 wenzelm 2005-06-17 replaced obsolete theory_of_sign by theory_of_thm;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; Context.str_of_thy;
2005-06-17 wenzelm 2005-06-17 refer to HOL4_PROOFS setting; accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; proper treatment of Pure session;
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-06-17 wenzelm 2005-06-17 renamed sg_ref to thy_ref;
2005-06-17 wenzelm 2005-06-17 obsolete;
2005-06-17 wenzelm 2005-06-17 obsolete (see context.ML);
2005-06-17 haftmann 2005-06-17 (removed experimental file)
2005-06-17 wenzelm 2005-06-17 updated;
2005-06-17 quigley 2005-06-17 Multiple subgoals working.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-17 paulson 2005-06-17 grammar fix
2005-06-17 paulson 2005-06-17 removed redundant "open" declarations
2005-06-16 wenzelm 2005-06-16 tuned;
2005-06-16 paulson 2005-06-16 a few new integer lemmas
2005-06-16 nipkow 2005-06-16 *** empty log message ***
2005-06-16 haftmann 2005-06-16 isa-migrate ++
2005-06-16 nipkow 2005-06-16 *** empty log message ***
2005-06-16 nipkow 2005-06-16 *** empty log message ***
2005-06-16 haftmann 2005-06-16 isa-migrate ++
2005-06-16 haftmann 2005-06-16 isa-migrate ++
2005-06-16 haftmann 2005-06-16 isa-migrate ++
2005-06-16 haftmann 2005-06-16 added macos emacs hints
2005-06-16 haftmann 2005-06-16 isa-migrate ++
2005-06-15 huffman 2005-06-15 Domain package uses ContProc for beta reduction
2005-06-15 huffman 2005-06-15 allow theorem attributes on fixpat declarations
2005-06-15 huffman 2005-06-15 fixrec package now handles mutually-recursive definitions
2005-06-15 haftmann 2005-06-15 (undone experimental changes)
2005-06-15 haftmann 2005-06-15 subclassing done
2005-06-15 chaieb 2005-06-15 int -> IntInf.int
2005-06-15 nipkow 2005-06-15 added lemmas
2005-06-15 nipkow 2005-06-15 *** empty log message ***
2005-06-15 nipkow 2005-06-15 documented DUMMY
2005-06-14 huffman 2005-06-14 in domain declarations, selector names are now optional
2005-06-14 wenzelm 2005-06-14 use POLY instead of DISCGARB;
2005-06-14 wenzelm 2005-06-14 discontinued polyml-3.x; made cygwin functionality less intrusive; more quoting of expressions;
2005-06-14 wenzelm 2005-06-14 export cases_tac, induct_tac;