--- a/ProgTutorial/Package/Ind_General_Scheme.thy Sun Oct 25 15:26:03 2009 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy Sun Oct 25 16:12:05 2009 +0100
@@ -108,10 +108,10 @@
@{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
- meta-variable @{text "?P"}.
+ schematic variable @{text "?P"}.
In order to derive an induction principle for the predicate @{text "pred"},
- we first transform @{text ind} into the object logic and fix the meta-variables.
+ we first transform @{text ind} into the object logic and fix the schematic variables.
Hence we have to prove a formula of the form
@{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}