src/Tools/isac/Interpret/rewtools.sml
changeset 59310 14333576fb70
parent 59302 91564a5be356
child 59313 8f730d631591
     1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Sun Feb 05 16:39:37 2017 +0100
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Mon Feb 06 06:27:31 2017 +0100
     1.3 @@ -42,11 +42,16 @@
     1.4    val get_bdv_subst : term -> (term * term) list -> Selem.subs option * subst
     1.5    val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename
     1.6    val guh2theID : guh -> theID
     1.7 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.8 +  (*  NONE *)
     1.9  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.10    val trtas2str : (term * rule * (term * term list)) list -> string
    1.11    val eq_Thm : rule * rule -> bool
    1.12    val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string
    1.13  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.14 +
    1.15 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    1.16 +  (* NONE *)
    1.17  end 
    1.18  
    1.19  (**)