wenzelm [Fri, 17 Jun 2005 18:33:42 +0200] rev 16457
Context.names_of;
wenzelm [Fri, 17 Jun 2005 18:33:41 +0200] rev 16456
* Pure/TheoryDataFun: change of the argument structure;
* Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;
wenzelm [Fri, 17 Jun 2005 18:33:40 +0200] rev 16455
Sign.root_path, Sign.local_path;
wenzelm [Fri, 17 Jun 2005 18:33:39 +0200] rev 16454
removed obsolete theory_of_sign, theory_of_thm;
Context.draftN;
Context.begin_theory;
wenzelm [Fri, 17 Jun 2005 18:33:38 +0200] rev 16453
PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm [Fri, 17 Jun 2005 18:33:37 +0200] rev 16452
Context.DATA_FAIL;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:36 +0200] rev 16451
Context.PureN;
wenzelm [Fri, 17 Jun 2005 18:33:35 +0200] rev 16450
RuleCases.tactic;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:34 +0200] rev 16449
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
tuned;
wenzelm [Fri, 17 Jun 2005 18:33:33 +0200] rev 16448
(RAW_)METHOD_CASES: RuleCases.tactic;
accomodate change of TheoryDataFun;
wenzelm [Fri, 17 Jun 2005 18:33:32 +0200] rev 16447
Theory.add_typedecls;
Sign.local_path;
wenzelm [Fri, 17 Jun 2005 18:33:31 +0200] rev 16446
added map', fold;
changed join to pass key;
wenzelm [Fri, 17 Jun 2005 18:33:30 +0200] rev 16445
Table.fold;
wenzelm [Fri, 17 Jun 2005 18:33:29 +0200] rev 16444
Symtab.fold;
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;