src/Pure/CPure.thy

extended

(*  Title:      Pure/CPure.thy
    ID:         $Id$

The CPure theory -- Pure with alternative application syntax.
*)

theory CPure
imports Pure
begin

no_syntax
  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)

syntax
  "" :: "'a => cargs"  ("_")
  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)

end