generalized type for predicate went through the tests start_Take
authorwneuper
Thu, 14 Sep 2006 16:18:55 +0200
branchstart_Take
changeset 662ae3c14fdada4
parent 661 dfcdcbd43ab2
child 663 231221da44bc
generalized type for predicate went through the tests
src/sml/IsacKnowledge/Atools.thy
     1.1 --- a/src/sml/IsacKnowledge/Atools.thy	Thu Sep 14 16:14:01 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Atools.thy	Thu Sep 14 16:18:55 2006 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4    Arbfix, Undef    :: real
     1.5    dummy            :: real
     1.6  
     1.7 -  some'_occur'_in  :: "[real list, real] => bool" ("some'_of _ occur'_in _")
     1.8 -  occurs'_in       :: "[real     , real] => bool" ("_ occurs'_in _")
     1.9 +  some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
    1.10 +  occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
    1.11  
    1.12   "pow"   :: [real, real] => real    (infixr "^^^" 80)
    1.13  (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)