1.1 --- a/src/HOL/Prolog/Test.thy	Thu Feb 28 14:24:21 2013 +0100
     1.2 +++ b/src/HOL/Prolog/Test.thy	Thu Feb 28 14:29:54 2013 +0100
     1.3 @@ -26,52 +26,51 @@
     1.4  
     1.5  typedecl person
     1.6  
     1.7 -consts
     1.8 -  append  :: "['a list, 'a list, 'a list]            => bool"
     1.9 -  reverse :: "['a list, 'a list]                     => bool"
    1.10 +axiomatization
    1.11 +  append  :: "['a list, 'a list, 'a list]            => bool" and
    1.12 +  reverse :: "['a list, 'a list]                     => bool" and
    1.13  
    1.14 -  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
    1.15 -  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool"
    1.16 +  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" and
    1.17 +  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool" and
    1.18  
    1.19 -  bob     :: person
    1.20 -  sue     :: person
    1.21 -  ned     :: person
    1.22 +  bob     :: person and
    1.23 +  sue     :: person and
    1.24 +  ned     :: person and
    1.25  
    1.26 -  nat23   :: nat          ("23")
    1.27 -  nat24   :: nat          ("24")
    1.28 -  nat25   :: nat          ("25")
    1.29 +  nat23   :: nat          ("23") and
    1.30 +  nat24   :: nat          ("24") and
    1.31 +  nat25   :: nat          ("25") and
    1.32  
    1.33 -  age     :: "[person, nat]                          => bool"
    1.34 +  age     :: "[person, nat]                          => bool" and
    1.35  
    1.36 -  eq      :: "['a, 'a]                               => bool"
    1.37 +  eq      :: "['a, 'a]                               => bool" and
    1.38  
    1.39 -  empty   :: "['b]                                   => bool"
    1.40 -  add     :: "['a, 'b, 'b]                           => bool"
    1.41 -  remove  :: "['a, 'b, 'b]                           => bool"
    1.42 +  empty   :: "['b]                                   => bool" and
    1.43 +  add     :: "['a, 'b, 'b]                           => bool" and
    1.44 +  remove  :: "['a, 'b, 'b]                           => bool" and
    1.45    bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
    1.46 -
    1.47 -axioms
    1.48 -        append:  "append  []    xs  xs    ..
    1.49 -                  append (x#xs) ys (x#zs) :- append xs ys zs"
    1.50 -        reverse: "reverse L1 L2 :- (!rev_aux.
    1.51 +where
    1.52 +        append:  "\<And>x xs ys zs. append  []    xs  xs    ..
    1.53 +                  append (x#xs) ys (x#zs) :- append xs ys zs" and
    1.54 +        reverse: "\<And>L1 L2. reverse L1 L2 :- (!rev_aux.
    1.55                    (!L.          rev_aux  []    L  L )..
    1.56                    (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    1.57 -                  => rev_aux L1 L2 [])"
    1.58 +                  => rev_aux L1 L2 [])" and
    1.59  
    1.60 -        mappred: "mappred P  []     []    ..
    1.61 -                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
    1.62 -        mapfun:  "mapfun f  []     []      ..
    1.63 -                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
    1.64 +        mappred: "\<And>x xs y ys P. mappred P  []     []    ..
    1.65 +                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys" and
    1.66 +        mapfun:  "\<And>x xs ys f. mapfun f  []     []      ..
    1.67 +                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" and
    1.68  
    1.69          age:     "age bob 24 ..
    1.70                    age sue 23 ..
    1.71 -                  age ned 23"
    1.72 +                  age ned 23" and
    1.73  
    1.74 -        eq:      "eq x x"
    1.75 +        eq:      "\<And>x. eq x x" and
    1.76  
    1.77  (* actual definitions of empty and add is hidden -> yields abstract data type *)
    1.78  
    1.79 -        bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
    1.80 +        bag_appl: "\<And>A B X Y. bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
    1.81                                  empty    S1    &
    1.82                                  add A    S1 S2 &
    1.83                                  add B    S2 S3 &

     2.1 --- a/src/HOL/Prolog/Type.thy	Thu Feb 28 14:24:21 2013 +0100
     2.2 +++ b/src/HOL/Prolog/Type.thy	Thu Feb 28 14:29:54 2013 +0100
     2.3 @@ -10,14 +10,13 @@
     2.4  
     2.5  typedecl ty
     2.6  
     2.7 -consts
     2.8 -  bool    :: ty
     2.9 -  nat     :: ty
    2.10 -  arrow   :: "ty => ty => ty"       (infixr "->" 20)
    2.11 -  typeof  :: "[tm, ty] => bool"
    2.12 +axiomatization
    2.13 +  bool    :: ty and
    2.14 +  nat     :: ty and
    2.15 +  arrow   :: "ty => ty => ty"       (infixr "->" 20) and
    2.16 +  typeof  :: "[tm, ty] => bool" and
    2.17    anyterm :: tm
    2.18 -
    2.19 -axioms  common_typeof:   "
    2.20 +where common_typeof:   "
    2.21  typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
    2.22  
    2.23  typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    2.24 @@ -35,13 +34,13 @@
    2.25  typeof (M - N) nat :- typeof M nat & typeof N nat..
    2.26  typeof (M * N) nat :- typeof M nat & typeof N nat"
    2.27  
    2.28 -axioms good_typeof:     "
    2.29 +axiomatization where good_typeof:     "
    2.30  typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
    2.31  
    2.32 -axioms bad1_typeof:     "
    2.33 +axiomatization where bad1_typeof:     "
    2.34  typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
    2.35  
    2.36 -axioms bad2_typeof:     "
    2.37 +axiomatization where bad2_typeof:     "
    2.38  typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    2.39  
    2.40