wneuper/isa: test/Tools/isac/Test_Some

     1 theory Test_Some_meld imports Isac.Build_Thydata

     2 begin

     3 ML \<open>

     4   open Kernel;

     5   open Math_Engine;

     6   open LItool;                  arguments_from_model;

     7   open Env;

     8   open LI;               scan_dn;

     9   open Istate;

    10   open Specification;

    11   open Ctree;                  append_problem;

    12   open Program;

    13   open Prog_Tac;

    14   open Tactical;

    15   open Prog_Expr;

    16   open Auto_Prog;              rule2stac;

    17   open Input_Descript;

    18   open Specify;

    19   open Solve;                  (* NONE *)

    20   open ContextC;               transfer_asms_from_to;

    21   open Tactic;                 (* NONE *)

    22   open P_Model;                  (* NONE *)

    23   open Eval;                   get_pair;

    24   open TermC;                  atomt;

    25   open Rule;                   ThmC.string_of_thm;

    27   Know_Store.set_ref_last_thy @{theory};

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

    29 \<close>

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

    32 ML \<open>

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

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

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

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

    37 "xx"

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

    39 \<close> ML \<open>

    40 \<close>

    41 ML \<open>

    42 \<close> ML \<open>

    43 \<close> ML \<open>

    44 \<close>

    45 text \<open>

    46   declare [[show_types]]

    47   declare [[show_sorts]]

    48   find_theorems "?a <= ?a"

    50   print_theorems

    51   print_facts

    52   print_statement ""

    53   print_theory

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

    55   declare [[ML_print_depth = 999]]

    56   declare [[ML_exception_trace]]

    57 \<close>

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

    60 ML \<open>

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

    62 \<close> ML \<open>

    63 \<close> ML \<open>

    64 \<close> ML \<open>

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

    66 \<close>

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

    69 ML \<open>

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

    71 \<close> ML \<open>

    72 \<close> ML \<open>

    73 \<close> ML \<open>

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

    75 \<close>

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

    78 ML \<open>

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

    80 \<close> ML \<open>

    81 \<close> ML \<open>

    82 \<close> ML \<open>

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

    84 \<close>

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

    87 ML \<open>

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

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

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

    92 \<close>

    93 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 11 Jan 2023 11:38:01 +0100
changeset 60650	06ec8abfd3bc
parent 60608	5dabcc1c9235
permissions	-rw-r--r--