[isabelle] Illegal schematic goal statement



As should be clear from my previous posts, I continue trying to find Isabelle induction rules that correspond with the way my students learn induction. By accident I stumbled upon a file called How_To_Prove_it.thy, which suggests: "There are many more special induction rules. You can find all of them via the Find button...with the following search criteria: name: Nat name: induct." So I tried this, and I got 18 rules, some of which appear to apply to some of my situations (particularly Nat.dec_induct). However, I am now getting an error message which I have never seen before, when I try to enter one of these, exactly as it appears in the Query window, as a lemma. For example, the second one appears as Nat.nat_induct: ?P 0 ==> (\bigwedge n. ?P n ==> ?P (Suc n)) ==> ?P ?n . When I enter this as a lemma (in double quotes, of course) I get the message "Illegal schematic goal statement." Well, I can always take the question marks out, but why does Find Theorems find a theorem in a form that doesn't enter? (I've also tried it without the double quotes, and this time I get an outer syntax error on the \bigwedge .) Thanks! -WDMaurer
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.