1.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Aug 26 10:51:35 2023 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Sat Aug 26 11:37:16 2023 +0200
     1.3 @@ -138,6 +138,19 @@
     1.4  \<close>
     1.5  
     1.6  section \<open>code for copy & paste ===============================================================\<close>
     1.7 +text \<open>
     1.8 +  declare [[show_types]] 
     1.9 +  declare [[show_sorts]]
    1.10 +  find_theorems "?a <= ?a"
    1.11 +  
    1.12 +  print_theorems
    1.13 +  print_facts
    1.14 +  print_statement ""
    1.15 +  print_theory
    1.16 +  ML_command \<open>Pretty.writeln prt\<close>
    1.17 +  declare [[ML_print_depth = 999]]
    1.18 +  declare [[ML_exception_trace]]
    1.19 +\<close>
    1.20  ML \<open>
    1.21  \<close> ML \<open>
    1.22  "~~~~~ fun xxx , args:"; val () = ();
    1.23 @@ -151,6 +164,7 @@
    1.24  (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
    1.25  (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
    1.26  \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
    1.27 +
    1.28  val return_XXXXX = "XXXXX"
    1.29  \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
    1.30  (*//------------------ step into XXXXX -----------------------------------------------------\\*)
    1.31 @@ -166,7 +180,6 @@
    1.32  (*//------------------ inserted hidden code ------------------------------------------------\\*)
    1.33  (*\\------------------ inserted hidden code ------------------------------------------------//*)
    1.34  \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
    1.35 -
    1.36  \<close>
    1.37  ML \<open>
    1.38  \<close> ML \<open>
    1.39 @@ -174,10 +187,6 @@
    1.40  \<close> ML \<open>
    1.41  \<close>
    1.42  
    1.43 -ML \<open>
    1.44 -  (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
    1.45 -\<close>
    1.46 -
    1.47  section \<open>trials with Isabelle's functions\<close>
    1.48    ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.49    ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"