Fri, 17 Jun 2005 18:33:34 +0200 accomodate change of TheoryDataFun;
wenzelm [Fri, 17 Jun 2005 18:33:34 +0200] rev 16449
accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; tuned;
Fri, 17 Jun 2005 18:33:33 +0200 (RAW_)METHOD_CASES: RuleCases.tactic;
wenzelm [Fri, 17 Jun 2005 18:33:33 +0200] rev 16448
(RAW_)METHOD_CASES: RuleCases.tactic; accomodate change of TheoryDataFun;
Fri, 17 Jun 2005 18:33:32 +0200 Theory.add_typedecls;
wenzelm [Fri, 17 Jun 2005 18:33:32 +0200] rev 16447
Theory.add_typedecls; Sign.local_path;
Fri, 17 Jun 2005 18:33:31 +0200 added map', fold;
wenzelm [Fri, 17 Jun 2005 18:33:31 +0200] rev 16446
added map', fold; changed join to pass key;
Fri, 17 Jun 2005 18:33:30 +0200 Table.fold;
wenzelm [Fri, 17 Jun 2005 18:33:30 +0200] rev 16445
Table.fold;
Fri, 17 Jun 2005 18:33:29 +0200 Symtab.fold;
wenzelm [Fri, 17 Jun 2005 18:33:29 +0200] rev 16444
Symtab.fold;
Fri, 17 Jun 2005 18:33:28 +0200 type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm [Fri, 17 Jun 2005 18:33:28 +0200] rev 16443
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;
Fri, 17 Jun 2005 18:33:27 +0200 obsolete type sg is now an alias for Context.theory;
wenzelm [Fri, 17 Jun 2005 18:33:27 +0200] rev 16442
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;
Fri, 17 Jun 2005 18:33:26 +0200 added theorem_space;
wenzelm [Fri, 17 Jun 2005 18:33:26 +0200] rev 16441
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;
Fri, 17 Jun 2005 18:33:25 +0200 Context.theory_name;
wenzelm [Fri, 17 Jun 2005 18:33:25 +0200] rev 16440
Context.theory_name; tuned;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip