diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-11-27 16:21:27 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-11-27 16:21:27 +0000 |
| commit | 854fe0aac10c56372f2e185ab9b68379c232d33b (patch) | |
| tree | 203a687ac18b5188d96b8ee1e15920980dde5e2f /examples/logic/Prooftext.gf | |
| parent | a5232f7e5b8f6ca988696f3870f019113edb8d90 (diff) | |
AdvS and for_Prep in resource (except Russian)
Diffstat (limited to 'examples/logic/Prooftext.gf')
| -rw-r--r-- | examples/logic/Prooftext.gf | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf index e6a6c710c..3a5a61894 100644 --- a/examples/logic/Prooftext.gf +++ b/examples/logic/Prooftext.gf @@ -34,6 +34,9 @@ oper = \decl,a,b -> appendText decl (mkUtt (mkS (pred b a))) ; + theorem : Prop -> Proof -> Section + = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ; + assumption : Prop -> Decl = \p -> mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ; @@ -45,6 +48,8 @@ oper proof = overload { proof : Prop -> Proof = \p -> mkText (mkPhr p) TEmpty ; + proof : Str -> Proof + = \s -> {s = s ++ "." ; lock_Text = <>} ; proof : Adverb -> Prop -> Proof = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ; proof : Decl -> Proof @@ -76,4 +81,6 @@ oper refs : Refs -> Ref = \rs -> mkNP and_Conj rs ; + mkLabel : Str -> Label ; + } |