changeset 114:3ad2d97896d1

Now the antiqutation is correct for the type See https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-August/msg00032.html
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 24 Aug 2009 14:28:26 +0200
parents 4ca6534d5d2a
children c4e0cddc0d7d 7086a0fde0ca
files isabelle/TestProofExists.thy
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/isabelle/TestProofExists.thy	Mon Aug 24 11:10:42 2009 +0200
+++ b/isabelle/TestProofExists.thy	Mon Aug 24 14:28:26 2009 +0200
@@ -5,7 +5,7 @@
 ML {*
   case FindTheorems.find_theorems
       (ProofContext.init @{theory})
-      (SOME (Goal.init @{cterm "mono (f::nat \<Rightarrow> ('a::linorder)) \<Longrightarrow> e < f u \<longrightarrow> (\<forall>x<l. f x \<le> e) \<longrightarrow> e < f (binsearch f e l u) \<and>
+      (SOME (Goal.init @{cprop "mono (f::nat \<Rightarrow> ('a::linorder)) \<Longrightarrow> e < f u \<longrightarrow> (\<forall>x<l. f x \<le> e) \<longrightarrow> e < f (binsearch f e l u) \<and>
 (\<forall>x<binsearch f e l u. f x \<le> e)"}))
       (NONE)
       (true)