src/ZF/Coind/Language.thy
changeset 16417 9bc16273c2d4
parent 12595 0480d02221b8
child 35762 af3ff2ba4c54
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     4     Copyright   1995  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 theory Language = Main:
     7 theory Language imports Main begin
     8 
     8 
     9 consts
     9 consts
    10   Const :: i                    (* Abstract type of constants *)
    10   Const :: i                    (* Abstract type of constants *)
    11   c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
    11   c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
    12 
    12