author | haftmann |
Fri, 22 Feb 2008 16:31:37 +0100 | |
changeset 26114 | 53eb3ff08cce |
parent 26113 | ba5909699cc3 |
child 26115 | 3c38ef7cf54f |
--- a/src/HOL/Library/Eval_Witness.thy Fri Feb 22 12:01:57 2008 +0100 +++ b/src/HOL/Library/Eval_Witness.thy Fri Feb 22 16:31:37 2008 +0100 @@ -86,9 +86,9 @@ naturals, since ML integers are different. *} -lemma "\<exists>n::nat. n = 1" -apply (eval_witness "Isabelle_Eval.Suc Isabelle_Eval.Zero_nat") -done +(*lemma "\<exists>n::nat. n = 1" +apply (eval_witness "Suc Zero_nat") +done*) text {* Since polymorphism is not allowed, we must specify the