equal
deleted
inserted
replaced
42 text \<open> |
42 text \<open> |
43 declare [[show_types]] |
43 declare [[show_types]] |
44 declare [[show_sorts]] |
44 declare [[show_sorts]] |
45 find_theorems "?a <= ?a" |
45 find_theorems "?a <= ?a" |
46 |
46 |
47 print_theorems |
47 print_theorems |
48 print_facts |
48 print_facts |
49 print_statement "" |
49 print_statement "" |
50 print_theory |
50 print_theory |
51 ML_command \<open>Pretty.writeln prt\<close> |
51 ML_command \<open>Pretty.writeln prt\<close> |
52 declare [[ML_print_depth = 999]] |
52 declare [[ML_print_depth = 999]] |
53 declare [[ML_exception_trace]] |
53 declare [[ML_exception_trace]] |
54 \<close> |
54 \<close> |
55 |
55 |
56 section \<open>===================================================================================\<close> |
56 section \<open>===================================================================================\<close> |
57 section \<open>===== ============================================================================\<close> |
57 section \<open>===== ============================================================================\<close> |