src/Pure/CPure.thy
author wenzelm
Mon Apr 07 21:29:46 2008 +0200 (2008-04-07)
changeset 26572 9178a7f4c4c8
parent 26435 bdce320cd426
permissions -rw-r--r--
prefer plain ASCII here;
wenzelm@15804
     1
(*  Title:      Pure/CPure.thy
wenzelm@15804
     2
    ID:         $Id$
wenzelm@15804
     3
wenzelm@15804
     4
The CPure theory -- Pure with alternative application syntax.
wenzelm@15804
     5
*)
wenzelm@15804
     6
wenzelm@15804
     7
theory CPure
wenzelm@15804
     8
imports Pure
wenzelm@15804
     9
begin
wenzelm@15804
    10
wenzelm@26435
    11
no_syntax
wenzelm@26435
    12
  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
wenzelm@26435
    13
  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
wenzelm@26435
    14
wenzelm@26435
    15
syntax
wenzelm@26435
    16
  "" :: "'a => cargs"  ("_")
wenzelm@26435
    17
  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
wenzelm@26435
    18
  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
wenzelm@26435
    19
  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
wenzelm@15804
    20
wenzelm@15804
    21
end