diff -r 9cf3bc448210 -r be6538c7b41d ProgTutorial/Package/Ind_General_Scheme.thy --- 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 \ rules[preds := ?Ps] \ ?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 \ orules[preds := Ps] \ P zs"}