theory Test_Some_meld imports Isac.Build_Thydata

begin 

ML \<open>

  open Kernel;

  open Math_Engine;

  open LItool;                  arguments_from_model;

  open Env;

  open LI;               scan_dn;

  open Istate;

  open Specification;

  open Ctree;                  append_problem;

  open Program;

  open Prog_Tac;

  open Tactical;

  open Prog_Expr;

  open Auto_Prog;              rule2stac;

  open Input_Descript;

  open Specify;

  open Solve;                  (* NONE *)

  open ContextC;               transfer_asms_from_to;

  open Tactic;                 (* NONE *)

  open P_Model;                  (* NONE *)

  open Eval;                   get_pair;

  open TermC;                  atomt;

  open Rule;                   ThmC.string_of_thm;

  Know_Store.set_ref_last_thy @{theory};

  (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)

\<close>

section \<open>code for copy & paste ===============================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();

(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*);

"xx"

^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*)

\<close> ML \<open>

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

text \<open>

  declare [[show_types]] 

  declare [[show_sorts]]            

  find_theorems "?a <= ?a"

  print_theorems

  print_facts

  print_statement ""

  print_theory

  ML_command \<open>Pretty.writeln prt\<close>

  declare [[ML_print_depth = 999]]

  declare [[ML_exception_trace]]

\<close>

section \<open>===================================================================================\<close>

ML \<open>

"~~~~~ fun xxx, args:"; val () = ();

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

"~~~~~ fun xxx, args:"; val () = ();

\<close>

section \<open>===================================================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

\<close>

section \<open>===================================================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

\<close>

section \<open>code for copy & paste ===============================================================\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

\<close>

end