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