# [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.*