src/HOL/Induct/Term.thy
changeset 18461 9125d278fdc8
parent 16417 9bc16273c2d4
child 36862 952b2b102a0a
equal deleted inserted replaced
18460:9a1458cb2956 18461:9125d278fdc8
    42 
    42 
    43 lemma
    43 lemma
    44   assumes var: "!!v. P (Var v)"
    44   assumes var: "!!v. P (Var v)"
    45     and app: "!!f ts. list_all P ts ==> P (App f ts)"
    45     and app: "!!f ts. list_all P ts ==> P (App f ts)"
    46   shows term_induct2: "P t"
    46   shows term_induct2: "P t"
    47 and "list_all P ts"
    47     and "list_all P ts"
    48   apply (induct t and ts)
    48   apply (induct t and ts)
    49      apply (rule var)
    49      apply (rule var)
    50     apply (rule app)
    50     apply (rule app)
    51     apply assumption
    51     apply assumption
    52    apply simp_all
    52    apply simp_all