blob: 1f56cb35e066cc7c5bfe5b0434f39e338210a16b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* This is a test of tracing output for Isabelle. *)
theory trace_simp imports Main begin
text {*
this produces massive amount of simplifier trace, but terminates
eventually: *}
ML {* Config.put trace_simp true *}
ML {* reset quick_and_dirty *}
datatype ord = Zero | Succ ord | Limit "nat => ord"
(* testing comment here *)
text {* this one loops forever *}
lemma "ALL x. f x = g(f(g(x))) ==> f [] = f [] @ []"
apply simp
|
