wneuper/isa: test/Tools/isac/Test_Some

     1 theory Test_Some_meld imports Isac.Build_Thydata

     2 begin

     3 ML \<open>

     4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)

     5                       (* these vvv test, if funs are intermediately opened in structure

     6                          in case of errors here consider ~~/xtest-to-coding.sh      *)

     7   open Kernel;

     8   open Math_Engine;            CalcTreeTEST;

     9   open LItool.;                  arguments_from_model;

    10   open Env;

    11   open Exec;

    12   open LI;               scan_dn;

    13   open Istate;

    14   open Inform;                 cas_input;

    15   open Rtools;                 .trtas2str;

    16   open Chead;                  pt_extract;

    17   open Generate;               (* NONE *)

    18   open Ctree;                  append_problem;

    19   open Program;

    20   open Prog_Tac;

    21   open Tactical;

    22   open Prog_Expr;

    23   open Auto_Prog;              rule2stac;

    24   open Input_Descript;

    25   open Specify;                show_ptyps;

    26   open ApplicableOLD;             mk_set;

    27   open Solve;                  (* NONE *)

    28   open Selem;                  e_fmz;

    29   open Stool;                  (* NONE *)

    30   open ContextC;               transfer_asms_from_to;

    31   open Tactic;                 (* NONE *)

    32   open Model;                  (* NONE *)

    33   open Rewrite;                mk_thm;

    34   open Eval;                   get_pair;

    35   open TermC;                  atomt;

    36   open Celem;                  e_pbt;

    37   open Rule;                   ThmC.string_of_thm;

    38 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    39 \<close>

    40 ML_file "Calcelements/libraryC.sml"

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

    43 ML \<open>

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

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

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

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

    48 "xx"

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

    50 \<close> ML \<open>

    51 \<close>

    52 ML \<open>

    53 \<close> ML \<open>

    54 \<close> ML \<open>

    55 \<close>

    56 text \<open>

    57   declare [[show_types]]

    58   declare [[show_sorts]]

    59   find_theorems "?a <= ?a"

    61   print_theorems

    62   print_facts

    63   print_statement ""

    64   print_theory

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

    66   declare [[ML_print_depth = 999]]

    67   declare [[ML_exception_trace]]

    68 \<close>

    69 ML \<open>

    70 (*========== inhibit exn WN130909 TODO =========================================================

    71 ============ inhibit exn WN130909 TODO ========================================================*)

    72 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    73 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)

    74 \<close>

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

    77 ML \<open>

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

    79 \<close> ML \<open>

    80 \<close> ML \<open>

    81 \<close> ML \<open>

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

    83 \<close>

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

    86 ML \<open>

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

    88 \<close> ML \<open>

    89 \<close> ML \<open>

    90 \<close> ML \<open>

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

    92 \<close>

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

    95 ML \<open>

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

    97 \<close> ML \<open>

    98 \<close> ML \<open>

    99 \<close> ML \<open>

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

   101 \<close>

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

   104 ML \<open>

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

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

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

   109 \<close>

   110 end

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 29 Apr 2020 12:30:51 +0200
changeset 59920	33913fe24685
parent 59906	cc8df204dcb6
child 59941	602bf61dc6df
permissions	-rw-r--r--