Lines Matching defs:Level
1 \part{Using Isabelle from the ML Top-Level}\label{chap:getting}
475 {\out Level 0}
486 {\out Level 1}
495 {\out Level 2}
501 At Level~2 there are three subgoals, each provable by assumption. We
507 {\out Level 3}
515 {\out Level 4}
522 {\out Level 5}
550 {\out Level 0}
555 {\out Level 1}
564 {\out Level 2}
577 {\out Level 3}
585 {\out Level 4}
591 {\out Level 5}
602 {\out Level 6}
634 {\out Level 0}
639 {\out Level 1}
650 {\out Level 2}
660 {\out Level 3}
675 {\out Level 0}
680 {\out Level 1}
688 {\out Level 2}
692 Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we
716 {\out Level 0}
721 {\out Level 1}
731 {\out Level 2}
736 {\out Level 3}
744 {\out Level 4}
749 {\out Level 5}
771 {\out Level 1}
778 {\out Level 2}
783 {\out Level 3}
791 {\out Level 4}
796 {\out Level 5}
804 {\out Level 6}
817 {\out Level 0}
828 {\out Level 1}
844 {\out Level 0}
849 {\out Level 1}
859 {\out Level 2}
868 {\out Level 3}
880 {\out Level 4}
888 {\out Level 5}
915 {\out Level 0}
926 {\out Level 1}
937 {\out Level 0}
947 {\out Level 1}