src/HOL/Induct/Term.thy
changeset 12937 0c4fd7529467
parent 12171 dc87f33db447
child 14981 e73f8140af78
equal deleted inserted replaced
12936:84eb6c75cfe3 12937:0c4fd7529467
    40 
    40 
    41 
    41 
    42 text {* \medskip Alternative induction rule *}
    42 text {* \medskip Alternative induction rule *}
    43 
    43 
    44 lemma
    44 lemma
    45   (assumes var: "!!v. P (Var v)"
    45   assumes var: "!!v. P (Var v)"
    46     and app: "!!f ts. list_all P ts ==> P (App f ts)")
    46     and app: "!!f ts. list_all P ts ==> P (App f ts)"
    47   term_induct2: "P t"
    47   shows term_induct2: "P t"
    48 and "list_all P ts"
    48 and "list_all P ts"
    49   apply (induct t and ts)
    49   apply (induct t and ts)
    50      apply (rule var)
    50      apply (rule var)
    51     apply (rule app)
    51     apply (rule app)
    52     apply assumption
    52     apply assumption