src/HOL/Induct/Comb.thy
changeset 9101 b643f4d7b9e9
parent 5184 9b8547a9496a
child 11359 29f8b00d7e1f
equal deleted inserted replaced
9100:9e081c812338 9101:b643f4d7b9e9
    11     Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    11     Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    12     Report 265, University of Cambridge Computer Laboratory, 1992.
    12     Report 265, University of Cambridge Computer Laboratory, 1992.
    13 *)
    13 *)
    14 
    14 
    15 
    15 
    16 Comb = Datatype +
    16 Comb = Main +
    17 
    17 
    18 (** Datatype definition of combinators S and K, with infixed application **)
    18 (** Datatype definition of combinators S and K, with infixed application **)
    19 datatype comb = K
    19 datatype comb = K
    20               | S
    20               | S
    21               | "#" comb comb (infixl 90)
    21               | "#" comb comb (infixl 90)