equal
deleted
inserted
replaced
99 open Rtools; trtas2str; |
99 open Rtools; trtas2str; |
100 open Chead; pt_extract; |
100 open Chead; pt_extract; |
101 open Generate; (* NONE *) |
101 open Generate; (* NONE *) |
102 open Ctree; append_problem; |
102 open Ctree; append_problem; |
103 open Prog_Tac; |
103 open Prog_Tac; |
104 open Input_Descript; |
104 open Tactical; |
|
105 open Prog_Expr; |
|
106 (*open Auto_Prog;*) |
105 open Specify; show_ptyps; |
107 open Specify; show_ptyps; |
106 open Applicable; mk_set; |
108 open Applicable; mk_set; |
107 open Solve; (* NONE *) |
109 open Solve; (* NONE *) |
108 open Selem; e_fmz; |
110 open Selem; e_fmz; |
109 open Stool; (* NONE *) |
111 open Stool; (* NONE *) |
114 open Rewrite; mk_thm; |
116 open Rewrite; mk_thm; |
115 open Calc; get_pair; |
117 open Calc; get_pair; |
116 open TermC; atomt; |
118 open TermC; atomt; |
117 open Celem; e_pbt; |
119 open Celem; e_pbt; |
118 open Rule; string_of_thm; |
120 open Rule; string_of_thm; |
119 open Tools; eval_lhs; |
|
120 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
121 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
121 \<close> |
122 \<close> |
122 |
123 |
123 ML \<open> |
124 ML \<open> |
124 "~~~~~ fun xxx, args:"; val () = (); |
125 "~~~~~ fun xxx, args:"; val () = (); |
509 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac. |
510 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac. |
510 -------------------------------------------------------------------------------- |
511 -------------------------------------------------------------------------------- |
511 WN120321.TODO rearrange theories: |
512 WN120321.TODO rearrange theories: |
512 Knowledge |
513 Knowledge |
513 : |
514 : |
514 Atools.thy |
515 Prog_Expr.thy |
515 ///Descript.thy --> ProgLang |
516 ///Descript.thy --> ProgLang |
516 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*) |
517 Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*) |
517 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy |
518 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy |
518 Interpret.thy are generated (simplifies xml structure for theories) |
519 Interpret.thy are generated (simplifies xml structure for theories) |
519 Program.thy |
520 Program.thy |
520 Tools.thy |
521 Tools.thy |
521 ListC.thy <--- first_Proglang_thy |
522 ListC.thy <--- first_Proglang_thy |