src/HOL/Induct/Term.thy
changeset 5717 0d28dbe484b6
parent 5191 8ceaa19f7717
child 5738 0d8698c15439
equal deleted inserted replaced
5716:a3d2a6b6693e 5717:0d28dbe484b6
    26   term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
    26   term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
    27 
    27 
    28 inductive "term(A)"
    28 inductive "term(A)"
    29   intrs
    29   intrs
    30     APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
    30     APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
    31   monos   "[list_mono]"
    31   monos   list_mono
    32 
    32 
    33 defs
    33 defs
    34   (*defining abstraction/representation functions for term list...*)
    34   (*defining abstraction/representation functions for term list...*)
    35   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
    35   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
    36   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
    36   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"