src/HOL/Lambda/InductTermi.thy
changeset 9102 c7ba07e3bbe8
parent 5717 0d28dbe484b6
child 9716 9be481b4bc85
equal deleted inserted replaced
9101:b643f4d7b9e9 9102:c7ba07e3bbe8
     7 Goes back to
     7 Goes back to
     8 Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
     8 Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
     9 Also rediscovered by Matthes and Joachimski.
     9 Also rediscovered by Matthes and Joachimski.
    10 *)
    10 *)
    11 
    11 
    12 InductTermi = Acc + ListBeta +
    12 InductTermi = ListBeta +
    13 
    13 
    14 consts IT :: dB set
    14 consts IT :: dB set
    15 inductive IT
    15 inductive IT
    16 intrs
    16 intrs
    17 VarI "rs : lists IT ==> (Var n)$$rs : IT"
    17 VarI "rs : lists IT ==> (Var n)$$rs : IT"