# HG changeset patch
# User wenzelm
# Date 1452547818 -3600
# Node ID a1b666aaac1a20964792f3555d9104fc4dc428b7
# Parent  324bc1ffba12e06bafb3a8b5428da04dbfe47a04
eliminated old defs;

diff -r 324bc1ffba12 -r a1b666aaac1a src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Jan 11 22:23:03 2016 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Jan 11 22:30:18 2016 +0100
@@ -28,15 +28,12 @@
  eq             ::      "['a,'a] => o"  (infixl "=" 50)
  True           ::      "o"
  False          ::      "o"
- Not            ::      "o => o"        ("~ _" [40] 40)
  conj           ::      "[o,o] => o"    (infixr "&" 35)
  disj           ::      "[o,o] => o"    (infixr "|" 30)
  imp            ::      "[o,o] => o"    (infixr "-->" 25)
- iff            ::      "[o,o] => o"    (infixr "<->" 25)
       (*Quantifiers*)
  All            ::      "('a => o) => o"        (binder "ALL " 10)
  Ex             ::      "('a => o) => o"        (binder "EX " 10)
- Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
       (*Rewriting gadgets*)
  NORM           ::      "o => o"
  norm           ::      "'a => 'a"
@@ -157,12 +154,15 @@
 
 (**** Definitions ****)
 
-defs
-not_def:              "~P == P-->False"
-iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
+definition Not :: "o => o"  ("~ _" [40] 40)
+  where not_def: "~P == P-->False"
+
+definition iff :: "[o,o] => o"  (infixr "<->" 25)
+  where "P<->Q == (P-->Q) & (Q-->P)"
 
 (*Unique existence*)
-ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+definition Ex1 :: "('a => o) => o"  (binder "EX! " 10)
+  where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
 
 (*Rewriting -- special constants to flag normalized terms and formulae*)
 axiomatization where