test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy
changeset 52101 c3f399ce32af
parent 42090 908dfde7cf75
child 59111 c730b643bc0e
     1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -71,8 +71,7 @@
     1.4    the internal representation of "a + b * 3". The '...' indicate that some 
     1.5    details are still hidden; further details are received this way:
     1.6  *}
     1.7 -ML {* print_depth 99;
     1.8 -  @{term "a + b * 9"}
     1.9 +ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5;
    1.10  *}
    1.11  text {* The internal representation is too comprehensive for several kinds of 
    1.12    inspection. Thus ISAC provides additional features, as we see below. First