test/Tools/isac/Test_Some.thy
changeset 48895 35751d90365e
parent 48894 1920135f13c9
child 52065 41f6e90abf36
     1.1 --- a/test/Tools/isac/Test_Some.thy	Sun Jun 30 17:27:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Jul 11 16:58:31 2013 +0200
     1.3 @@ -1,13 +1,19 @@
     1.4   
     1.5  theory Test_Some imports Isac 
     1.6 -  uses ("~~/test/Tools/isac/Interpret/calchead.sml")
     1.7 +  uses ("~~/test/Tools/isac/Interpret/inform.sml")
     1.8  begin
     1.9 -  use "~~/test/Tools/isac/Interpret/calchead.sml"
    1.10 +  use "~~/test/Tools/isac/Interpret/inform.sml"
    1.11  
    1.12  declare [[show_types]] 
    1.13  declare [[show_sorts]]
    1.14  find_theorems "?a <= ?a"
    1.15  
    1.16 +print_facts
    1.17 +print_statement ""
    1.18 +print_theory 
    1.19 +
    1.20 +ML {*
    1.21 +*}
    1.22  ML {* (*==================*)
    1.23  *}
    1.24  ML {*
    1.25 @@ -18,15 +24,17 @@
    1.26  *}
    1.27  ML {*
    1.28  *}
    1.29 -ML {*
    1.30 -*}
    1.31 -ML {* (*/==================\*)
    1.32 +ML {* (*==================*)
    1.33  *}
    1.34  ML {*
    1.35  *}
    1.36  ML {*
    1.37  *}
    1.38 -ML {* (*\==================/*)
    1.39 +ML {*
    1.40 +*}
    1.41 +ML {*
    1.42 +*}
    1.43 +ML {* (*==================*)
    1.44  "~~~~~ fun , args:"; val () = ();
    1.45  
    1.46  "~~~~~ to  return val:"; val () = ();
    1.47 @@ -34,8 +42,8 @@
    1.48  *}
    1.49  end
    1.50  
    1.51 -(*========== inhibit exn WN1130630 maximum example broken =========================
    1.52 -============ inhibit exn WN1130630 maximum example broken =======================*)
    1.53 +(*========== inhibit exn WN1130701 broken already in 2009-2 =======================
    1.54 +============ inhibit exn WN1130701 broken already in 2009-2 =====================*)
    1.55  (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
    1.56  ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
    1.57