src/Doc/Tutorial/Rules/Basic.thy

 oops
 
 
 text{*unification failure trace *}
 
-ML "trace_unify_fail := true"
+declare [[unify_trace_failure = true]]
 
 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 apply assumption

 Clash: == =/= Trueprop
 Clash: == =/= Trueprop
 *}
 oops
 
-ML "trace_unify_fail := false"
+declare [[unify_trace_failure = false]]
 
 
 text{*Quantifiers*}
 
 text {*