src/HOL/Induct/Term.thy
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 18461 9125d278fdc8
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     3     Author:     Stefan Berghofer,  TU Muenchen
     3     Author:     Stefan Berghofer,  TU Muenchen
     4 *)
     4 *)
     5 
     5 
     6 header {* Terms over a given alphabet *}
     6 header {* Terms over a given alphabet *}
     7 
     7 
     8 theory Term = Main:
     8 theory Term imports Main begin
     9 
     9 
    10 datatype ('a, 'b) "term" =
    10 datatype ('a, 'b) "term" =
    11     Var 'a
    11     Var 'a
    12   | App 'b "('a, 'b) term list"
    12   | App 'b "('a, 'b) term list"
    13 
    13