wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports Isac.Build_Isac

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

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

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

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

    10   open Kernel;

    11   open Math_Engine;

    12   open Test_Code;              CalcTreeTEST;

    13   open LItool;                 arguments_from_model;

    14   open Sub_Problem;

    15   open Fetch_Tacs;

    16   open Step

    17   open Env;

    18   open LI;                     scan_dn;

    19   open Istate;

    20   open Error_Fill_Pattern;

    21   open Error_Fill_Def;

    22   open In_Chead;

    23   open Rtools;                 trtas2str;

    24   open Chead;                  pt_extract;

    25   open Generate;               (* NONE *)

    26   open Ctree;                  append_problem;

    27   open Pos;

    28   open Program;

    29   open Prog_Tac;

    30   open Tactical;

    31   open Prog_Expr;

    32   open Auto_Prog;              rule2stac;

    33   open Input_Descript;

    34   open Specify;                show_ptyps;

    35   open SpecifyNEW;

    36   open Applicable;             mk_set;

    37   open Step_Specify;

    38   open Step_Solve;

    39   open Step;

    40   open Solve;                  (* NONE *)

    41   open Selem;                  e_fmz;

    42   open Stool;                  (* NONE *)

    43   open ContextC;               transfer_asms_from_to;

    44   open Tactic;                 (* NONE *)

    45   open Model;                  (* NONE *)

    46   open Rewrite;

    47   open Eval;                   get_pair;

    48   open TermC;                  atomt;

    49   open Celem;                  e_pbt;

    50   open Rule;

    51   open Rule_Set

    52   open Exec_Def

    53   open ThyC

    54   open ThmC_Def

    55   open ThmC

    56   open Rewrite_Ord

    57   open UnparseC

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

    59 \<close>

    60 ML_file "BaseDefinitions/libraryC.sml"

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

    63 ML \<open>

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

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

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

    67 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);

    68 "xx"

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

    70 \<close> ML \<open>

    71 \<close>

    72 ML \<open>

    73 \<close> ML \<open>

    74 \<close> ML \<open>

    75 \<close>

    76 text \<open>

    77   declare [[show_types]]

    78   declare [[show_sorts]]

    79   find_theorems "?a <= ?a"

    81   print_theorems

    82   print_facts

    83   print_statement ""

    84   print_theory

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

    86   declare [[ML_print_depth = 999]]

    87   declare [[ML_exception_trace]]

    88 \<close>

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

    91 ML \<open>

    92 \<close> ML \<open>

    93 \<close> ML \<open>

    94 \<close>

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

    97 ML \<open>

    98 \<close> ML \<open>

    99 \<close> ML \<open>

   100 \<close> ML \<open>

   101 \<close>

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

   104 ML \<open>

   105 \<close> ML \<open>

   106 \<close> ML \<open>

   107 \<close>

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

   110 ML \<open>

   111 \<close> ML \<open>

   112 \<close> ML \<open>

   113 \<close>

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

   116 ML \<open>

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

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

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

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

   121 "xx"

   122 ^ "xxx"   (*+*)

   123 \<close>

   124 end

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 20 Apr 2020 15:54:19 +0200
changeset 59892	b8cfae027755
parent 59886	106e7d8723ca
child 59906	cc8df204dcb6
permissions	-rw-r--r--