wneuper/isa: test/Tools/isac/Test_Theory.thy@b7a2ad3b3d45

     1 (* use this theory for tests before Build_Isac.thy has succeeded *)

     2 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

     3 begin

     4 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

     5 (* ATTENTION: tests with Test_Code.init_calc, CalcTree @{context} do NOT work here, because Thy_Info.get_theory

     6   requires session Isac, see $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory *)

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

     9 ML \<open>

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

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

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

    13 "~~~~~ continue fun xxx"; val () = ();

    14 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

    15 "xx"

    16 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

    17 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

    18 (*//------------------ adhoc inserted n ----------------------------------------------------\\*)

    19 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

    20 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

    22 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

    23 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

    24 (*keep for continuing YYYYY*)

    25 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)

    26 (*-------------------- continuing XXXXX ------------------------------------------------------*)

    27 (*kept for continuing YYYYY*)

    28 (*-------------------- stop step into XXXXX --------------------------------------------------*)

    29 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

    30 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

    31 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

    33 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

    34 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

    35 (*/------------------- check within XXXXX ---------------------------------------------------\*)

    36 (*\------------------- check within XXXXX ---------------------------------------------------/*)

    37 (*/------------------- check result of XXXXX ------------------------------------------------\*)

    38 (*\------------------- check result of XXXXX ------------------------------------------------/*)

    39 (* final test ... ----------------------------------------------------------------------------*)

    41 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

    42 (*//------------------ inserted hidden code ------------------------------------------------\\*)

    43 (*\\------------------ inserted hidden code ------------------------------------------------//*)

    44 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

    46 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

    47 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

    48 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

    49 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

    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>

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

    71 ML \<open>

    72 \<close> ML \<open>

    73 \<close> ML \<open>

    74 \<close> ML \<open>

    75 \<close> ML \<open>

    76 \<close> ML \<open>

    77 \<close> ML \<open>

    78 \<close>

    80 section \<open>=========="Minisubpbl/100-init-rootpbl.sml"========================================\<close>

    81 ML \<open>

    82 \<close> ML \<open>

    83 \<close> ML \<open>

    84 \<close> ML \<open>

    85 \<close> ML \<open>

    86 \<close> ML \<open>

    87 \<close> ML \<open>

    88 \<close>

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

    91 ML \<open>

    92 \<close> ML \<open>

    93 \<close> ML \<open>

    94 \<close> ML \<open>

    95 \<close> ML \<open>

    96 \<close> ML \<open>

    97 \<close> ML \<open>

    98 \<close>

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

   101 ML \<open>

   102 \<close> ML \<open>

   103 \<close> ML \<open>

   104 \<close> ML \<open>

   105 \<close> ML \<open>

   106 \<close> ML \<open>

   107 \<close> ML \<open>

   108 \<close> ML \<open>

   109 \<close>

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

   112 ML \<open>

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

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

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

   116 "~~~~~ continue fun xxx"; val () = ();

   117 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

   118 "xx"

   119 ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

   120 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

   121  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

   122 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

   123 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

   125 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

   126 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

   127 (*keep for continuing YYYYY*)

   128 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)

   129 (*-------------------- continuing XXXXX ------------------------------------------------------*)

   130 (*kept for continuing XXXXX*)

   131 (*-------------------- stop step into XXXXX --------------------------------------------------*)

   132 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

   133 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

   134 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

   136 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

   137 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

   138 (*/------------------- check within XXXXX ---------------------------------------------------\*)

   139 (*\------------------- check within XXXXX ---------------------------------------------------/*)

   140 (*/------------------- check result of XXXXX ------------------------------------------------\*)

   141 (*\------------------- check result of XXXXX ------------------------------------------------/*)

   142 (* final test ... ----------------------------------------------------------------------------*)

   144 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

   145 (*//------------------ inserted hidden code ------------------------------------------------\\*)

   146 (*\\------------------ inserted hidden code ------------------------------------------------//*)

   147 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

   149 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

   150 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

   151 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

   152 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

   153 \<close>

   154 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 25 Jan 2023 15:52:33 +0100
changeset 60651	b7a2ad3b3d45
parent 60629	20c3d272d79c
child 60658	1c089105f581
permissions	-rw-r--r--