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

theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

  "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

begin                                                                            

ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

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

text \<open>

  declare [[show_types]] 

  declare [[show_sorts]]

  find_theorems "?a <= ?a"

  print_theorems

  print_facts

  print_statement ""

  print_theory

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

  declare [[ML_print_depth = 999]]

  declare [[ML_exception_trace]]

\<close>

(** )

  (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

( **)

ML \<open>

\<close> ML \<open>

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

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

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

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

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

"xx"

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

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

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

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

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

\<close> ML \<open> (*//----------- setup test data for XXXXX -------------------------------------------\\*)

(*//------------------ setup test data for XXXXX -------------------------------------------\\*)

(*\\------------------ setup test data for XXXXX -------------------------------------------//*)

\<close> ML \<open> (*\\----------- setup test data for XXXXX -------------------------------------------//*)

val return_XXXXX = "XXXXX"

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

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

\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)

(*||------------------ contine XXXXX ---------------------------------------------------------*)

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

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

val "XXXXX" = return_XXXXX;

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

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

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

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

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

\<close> ML \<open>

\<close>

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

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

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

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

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

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

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

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

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end