src/FOLP/IFOLP.thy
changeset 35113 1a0c129bb2e0
parent 32740 9dd0a2f83429
child 35128 c1ad622e90e4
     1.1 --- a/src/FOLP/IFOLP.thy	Thu Feb 11 22:06:37 2010 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Thu Feb 11 22:19:58 2010 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4  
     1.5  consts
     1.6        (*** Judgements ***)
     1.7 - "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
     1.8   Proof          ::   "[o,p]=>prop"
     1.9   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    1.10  
    1.11 @@ -66,6 +65,8 @@
    1.12  
    1.13  local
    1.14  
    1.15 +syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
    1.16 +
    1.17  ML {*
    1.18  
    1.19  (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    1.20 @@ -74,12 +75,12 @@
    1.21  fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
    1.22  
    1.23  fun proof_tr' [P,p] =
    1.24 -    if !show_proofs then Const("@Proof",dummyT) $ p $ P
    1.25 -    else P  (*this case discards the proof term*);
    1.26 +  if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
    1.27 +  else P  (*this case discards the proof term*);
    1.28  *}
    1.29  
    1.30 -parse_translation {* [("@Proof", proof_tr)] *}
    1.31 -print_translation {* [("Proof", proof_tr')] *}
    1.32 +parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
    1.33 +print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
    1.34  
    1.35  axioms
    1.36