ProgTutorial/Package/Ind_General_Scheme.thy
changeset 359 be6538c7b41d
parent 346 0fea8b7a14a1
child 517 d8c376662bb4
--- 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"}