src/HOL/Induct/ABexp.thy
changeset 58249 180f1b3508ed
parent 46914 c2ca2c3d23a6
child 58310 91ea607a34d8
equal deleted inserted replaced
58248:25af24e1f37b 58249:180f1b3508ed
     6 
     6 
     7 theory ABexp
     7 theory ABexp
     8 imports Main
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 datatype 'a aexp =
    11 datatype_new 'a aexp =
    12     IF "'a bexp"  "'a aexp"  "'a aexp"
    12     IF "'a bexp"  "'a aexp"  "'a aexp"
    13   | Sum "'a aexp"  "'a aexp"
    13   | Sum "'a aexp"  "'a aexp"
    14   | Diff "'a aexp"  "'a aexp"
    14   | Diff "'a aexp"  "'a aexp"
    15   | Var 'a
    15   | Var 'a
    16   | Num nat
    16   | Num nat