# HG changeset patch
# User wenzelm
# Date 1126120029 -7200
# Node ID 5b1d47d920ce02d4bba3387518ae2ac2135c8f78
# Parent  1322ed8e0ee4d79c45fb0d399fc5cc6d92e358f8
converted to Isar theory format;

diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Func.ML
--- a/src/HOL/Prolog/Func.ML	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Func.ML	Wed Sep 07 21:07:09 2005 +0200
@@ -3,8 +3,6 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-open Func;
-
 val prog_Func = prog_HOHH @ [eval];
 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
 val p = ptac prog_Func 1;
@@ -12,6 +10,4 @@
 pgoal "eval ((S (S Z)) + (S Z)) ?X";
 
 pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
-			\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
-
-
+                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Func.thy	Wed Sep 07 21:07:09 2005 +0200
@@ -1,40 +1,41 @@
 (*  Title:    HOL/Prolog/Func.thy
     ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-untyped functional language, with call by value semantics 
 *)
 
-Func = HOHH +
+header {* Untyped functional language, with call by value semantics *}
 
-types tm
-
-arities tm :: type
+theory Func
+imports HOHH
+begin
 
-consts	abs	:: (tm => tm) => tm
-	app	:: tm => tm => tm
+typedecl tm
 
-	cond	:: tm => tm => tm => tm
-	fix	:: (tm => tm) => tm
+consts
+  abs     :: "(tm => tm) => tm"
+  app     :: "tm => tm => tm"
+
+  cond    :: "tm => tm => tm => tm"
+  "fix"   :: "(tm => tm) => tm"
 
-	true,
-	false	:: tm
-	"and"	:: tm => tm => tm	(infixr 999)
-	"eq"	:: tm => tm => tm	(infixr 999)
+  true    :: tm
+  false   :: tm
+  "and"   :: "tm => tm => tm"       (infixr 999)
+  "eq"    :: "tm => tm => tm"       (infixr 999)
 
-	"0"	:: tm			("Z")
-	S	:: tm => tm
+  "0"     :: tm                   ("Z")
+  S       :: "tm => tm"
 (*
-	"++", "--",
-	"**"	:: tm => tm => tm	(infixr 999)
+        "++", "--",
+        "**"    :: tm => tm => tm       (infixr 999)
 *)
-	eval	:: [tm, tm] => bool
+        eval    :: "[tm, tm] => bool"
 
-arities tm :: plus
-arities tm :: minus
-arities tm :: times
+instance tm :: plus ..
+instance tm :: minus ..
+instance tm :: times ..
 
-rules	eval "
+axioms   eval: "
 
 eval (abs RR) (abs RR)..
 eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
@@ -47,7 +48,7 @@
 eval false false..
 eval (P and Q) true  :- eval P true  & eval Q true ..
 eval (P and Q) false :- eval P false | eval Q false..
-eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1.. 
+eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1..
 eval (A2 eq B2) false :- True..
 
 eval Z Z..
@@ -59,4 +60,6 @@
 eval ( Z    * M) Z..
 eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/HOHH.ML
--- a/src/HOL/Prolog/HOHH.ML	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/HOHH.ML	Wed Sep 07 21:07:09 2005 +0200
@@ -3,11 +3,9 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-open HOHH;
-
 exception not_HOHH;
 
-fun isD t = case t of 
+fun isD t = case t of
     Const("Trueprop",_)$t     => isD t
   | Const("op &"  ,_)$l$r     => isD l andalso isD r
   | Const("op -->",_)$l$r     => isG l andalso isD r
@@ -24,7 +22,7 @@
   | Bound _ (* rigid atom *)  => true
   | Free  _ (* rigid atom *)  => true
   | _    (* flexible atom,
-	    anything else *)  => false
+            anything else *)  => false
 and
     isG t = case t of
     Const("Trueprop",_)$t     => isG t
@@ -38,85 +36,85 @@
   | Const("True",_)           => true
   | Const("not",_)$_          => false
   | Const("False",_)          => false
-  | _ (* atom *)	      => true;
+  | _ (* atom *)              => true;
 
-val check_HOHH_tac1 = PRIMITIVE (fn thm => 
-	if isG (concl_of thm) then thm else raise not_HOHH);
-val check_HOHH_tac2 = PRIMITIVE (fn thm => 
-	if forall isG (prems_of thm) then thm else raise not_HOHH);
-fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm) 
-			then thm else raise not_HOHH);
+val check_HOHH_tac1 = PRIMITIVE (fn thm =>
+        if isG (concl_of thm) then thm else raise not_HOHH);
+val check_HOHH_tac2 = PRIMITIVE (fn thm =>
+        if forall isG (prems_of thm) then thm else raise not_HOHH);
+fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
+                        then thm else raise not_HOHH);
 
-fun atomizeD thm = let 
+fun atomizeD thm = let
     fun at  thm = case concl_of thm of
       _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
-					"?"^(if s="P" then "PP" else s))] spec))
+                                        "?"^(if s="P" then "PP" else s))] spec))
     | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
     | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
-    | _				    => [thm]
+    | _                             => [thm]
 in map zero_var_indexes (at thm) end;
 
 val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
-	all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
-	imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
-	imp_conjR,	  (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
-	imp_all];	  (* "((!x. D) :- G) = (!x. D :- G)" *)
+        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
+        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
+        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
-(*val hyp_resolve_tac = METAHYPS (fn prems => 
-				  resolve_tac (List.concat (map atomizeD prems)) 1);
+(*val hyp_resolve_tac = METAHYPS (fn prems =>
+                                  resolve_tac (List.concat (map atomizeD prems)) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
-	fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
-	|   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
-	|   ap t			  = 			    (0,false,t);
+        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
+        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
+        |   ap t                          =                         (0,false,t);
 (*
-	fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
-	|   rep_goal (Const ("==>",_)$s$t)	   = 
-			(case rep_goal t of (l,t) => (s::l,t))
-	|   rep_goal t				   = ([]  ,t);
-	val (prems, Const("Trueprop", _)$concl) = rep_goal 
-						(#3(dest_state (st,i)));
+        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
+        |   rep_goal (Const ("==>",_)$s$t)         =
+                        (case rep_goal t of (l,t) => (s::l,t))
+        |   rep_goal t                             = ([]  ,t);
+        val (prems, Const("Trueprop", _)$concl) = rep_goal
+                                                (#3(dest_state (st,i)));
 *)
-	val subgoal = #3(dest_state (st,i));
-	val prems = Logic.strip_assums_hyp subgoal;
-	val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
-	fun drot_tac k i = DETERM (rotate_tac k i);
-	fun spec_tac 0 i = all_tac
-	|   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
-	fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
-		      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
-	fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
-	|   same_head k (s$_)         (t$_)	    = same_head k s t
-	|   same_head k (Bound i)     (Bound j)	    = i = j + k
-	|   same_head _ _             _             = true;
-	fun mapn f n []      = []
-	|   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
-	fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
-		if same_head k t concl
-		then dup_spec_tac k i THEN 
-		     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
-		else no_tac);
-	val ptacs = mapn (fn n => fn t => 
-			  pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
-	in Library.foldl (op APPEND) (no_tac, ptacs) st end;
+        val subgoal = #3(dest_state (st,i));
+        val prems = Logic.strip_assums_hyp subgoal;
+        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
+        fun drot_tac k i = DETERM (rotate_tac k i);
+        fun spec_tac 0 i = all_tac
+        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
+        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
+                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
+        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
+        |   same_head k (s$_)         (t$_)         = same_head k s t
+        |   same_head k (Bound i)     (Bound j)     = i = j + k
+        |   same_head _ _             _             = true;
+        fun mapn f n []      = []
+        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
+        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
+                if same_head k t concl
+                then dup_spec_tac k i THEN
+                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
+                else no_tac);
+        val ptacs = mapn (fn n => fn t =>
+                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
+        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
 
 fun ptac prog = let
-  val proga = List.concat (map atomizeD prog)			(* atomize the prog *)
-  in	(REPEAT_DETERM1 o FIRST' [
-		rtac TrueI,			(* "True" *)
-		rtac conjI,			(* "[| P; Q |] ==> P & Q" *)
-		rtac allI,			(* "(!!x. P x) ==> ! x. P x" *)
-		rtac exI,			(* "P x ==> ? x. P x" *)
-		rtac impI THEN'			(* "(P ==> Q) ==> P --> Q" *)
-		  asm_full_simp_tac atomize_ss THEN'	(* atomize the asms *)
-		  (REPEAT_DETERM o (etac conjE))	(* split the asms *)
-		]) 
-	ORELSE' resolve_tac [disjI1,disjI2]	(* "P ==> P | Q","Q ==> P | Q"*)
-	ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
-		 THEN' (fn _ => check_HOHH_tac2))
+  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
+  in    (REPEAT_DETERM1 o FIRST' [
+                rtac TrueI,                     (* "True" *)
+                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
+                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
+                rtac exI,                       (* "P x ==> ? x. P x" *)
+                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
+                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
+                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
+                ])
+        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
+        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
+                 THEN' (fn _ => check_HOHH_tac2))
 end;
 
-fun prolog_tac prog = check_HOHH_tac1 THEN 
-		      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
+fun prolog_tac prog = check_HOHH_tac1 THEN
+                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
 
 val prog_HOHH = [];
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Wed Sep 07 21:07:09 2005 +0200
@@ -1,29 +1,30 @@
 (*  Title:    HOL/Prolog/HOHH.thy
     ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-higher-order hereditary Harrop formulas 
 *)
 
-HOHH = HOL +
+header {* Higher-order hereditary Harrop formulas *}
+
+theory HOHH
+imports HOL
+begin
 
 consts
 
-(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
-  "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
-  ":-"		:: [bool, bool] => bool		(infixl 29)
+(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
+  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
+  ":-"          :: "[bool, bool] => bool"         (infixl 29)
 
-(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
-			       | True | !x. G | D => G			*)
-(*","           :: [bool, bool] => bool		(infixr 35)*)
-  "=>"		:: [bool, bool] => bool		(infixr 27)
+(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
+                               | True | !x. G | D => G                  *)
+(*","           :: "[bool, bool] => bool"         (infixr 35)*)
+  "=>"          :: "[bool, bool] => bool"         (infixr 27)
 
 translations
 
-  "D :- G"	=>	"G --> D"
-  "D1 .. D2"	=>	"D1 & D2"
-(*"G1 , G2"	=>	"G1 & G2"*)
-  "D => G"	=>	"D --> G"
+  "D :- G"      =>      "G --> D"
+  "D1 .. D2"    =>      "D1 & D2"
+(*"G1 , G2"     =>      "G1 & G2"*)
+  "D => G"      =>      "D --> G"
 
 end
-
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Test.ML
--- a/src/HOL/Prolog/Test.ML	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Test.ML	Wed Sep 07 21:07:09 2005 +0200
@@ -3,8 +3,6 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-open Test;
-
 val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
 val p = ptac prog_Test 1;
@@ -44,7 +42,7 @@
 
 
 (*
-goal thy "f a = ?g a a & ?g = x"; 
+goal (the_context ()) "f a = ?g a a & ?g = x";
 by (rtac conjI 1);
 by (rtac refl 1);
 back();
@@ -107,11 +105,11 @@
 *)
 
 (* implication and disjunction in atom: *)
-goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
+goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
 by (fast_tac HOL_cs 1);
 
 (* disjunction in atom: *)
-goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
+goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
 by (step_tac HOL_cs 1);
 by (step_tac HOL_cs 1);
 by (step_tac HOL_cs 1);
@@ -119,7 +117,7 @@
 by (fast_tac HOL_cs 1);
 (*
 hangs:
-goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
+goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
 by (fast_tac HOL_cs 1);
 *)
 
@@ -144,4 +142,4 @@
 -> problem with DEPTH_SOLVE:
 Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
 Exception raised at run-time
-*)
\ No newline at end of file
+*)
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Test.thy	Wed Sep 07 21:07:09 2005 +0200
@@ -1,81 +1,85 @@
 (*  Title:    HOL/Prolog/Test.thy
     ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-basic examples 
 *)
 
-Test = HOHH +
+header {* Basic examples *}
 
-types nat
-arities nat :: type
+theory Test
+imports HOHH
+begin
 
-types 'a list
-arities list :: (type) type
+typedecl nat
+
+typedecl 'a list
 
-consts Nil   :: 'a list		 	 		 ("[]")
-       Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
+consts
+  Nil   :: "'a list"                                  ("[]")
+  Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
 
 syntax
   (* list Enumeration *)
-  "@list"     :: args => 'a list                          ("[(_)]")
+  "@list"     :: "args => 'a list"                          ("[(_)]")
 
 translations
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
 
-types   person
-arities person  :: type
+typedecl person
 
-consts  
-	append  :: ['a list, 'a list, 'a list]		  => bool
-	reverse :: ['a list, 'a list]			  => bool
+consts
+  append  :: "['a list, 'a list, 'a list]            => bool"
+  reverse :: "['a list, 'a list]                     => bool"
 
-	mappred	:: [('a => 'b => bool), 'a list, 'b list] => bool
-	mapfun	:: [('a => 'b), 'a list, 'b list]	  => bool
+  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
+  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool"
 
-	bob	:: person
-	sue	:: person
-	ned	:: person
+  bob     :: person
+  sue     :: person
+  ned     :: person
 
-	"23"	:: nat		("23")
-	"24"	:: nat		("24")
-	"25"	:: nat		("25")
+  "23"    :: nat          ("23")
+  "24"    :: nat          ("24")
+  "25"    :: nat          ("25")
 
-	age	:: [person, nat]			  => bool
+  age     :: "[person, nat]                          => bool"
 
-	eq	:: ['a, 'a]				  => bool
+  eq      :: "['a, 'a]                               => bool"
 
-	empty	:: ['b]					  => bool
-	add	:: ['a, 'b, 'b]				  => bool
-	remove	:: ['a, 'b, 'b]				  => bool
-	bag_appl:: ['a, 'a, 'a, 'a]			  => bool
+  empty   :: "['b]                                   => bool"
+  add     :: "['a, 'b, 'b]                           => bool"
+  remove  :: "['a, 'b, 'b]                           => bool"
+  bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
 
-rules   append	"append  []    xs  xs    ..
-		 append (x#xs) ys (x#zs) :- append xs ys zs"
-	reverse "reverse L1 L2 :- (!rev_aux. 
-		  (!L.          rev_aux  []    L  L )..
-		  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
-		  => rev_aux L1 L2 [])"
+axioms
+        append:  "append  []    xs  xs    ..
+                  append (x#xs) ys (x#zs) :- append xs ys zs"
+        reverse: "reverse L1 L2 :- (!rev_aux.
+                  (!L.          rev_aux  []    L  L )..
+                  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
+                  => rev_aux L1 L2 [])"
 
-	mappred "mappred P  []     []    ..
-		 mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
-	mapfun  "mapfun f  []     []      ..
-		 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
+        mappred: "mappred P  []     []    ..
+                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
+        mapfun:  "mapfun f  []     []      ..
+                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
 
-	age     "age bob 24 ..
-		 age sue 23 ..
-		 age ned 23"
+        age:     "age bob 24 ..
+                  age sue 23 ..
+                  age ned 23"
 
-	eq	"eq x x"
+        eq:      "eq x x"
 
 (* actual definitions of empty and add is hidden -> yields abstract data type *)
 
-	bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
-				empty    S1    &
-				add A    S1 S2 &
-				add B    S2 S3 &
-				remove X S3 S4 &
-				remove Y S4 S5 &
-				empty    S5)"
+        bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
+                                empty    S1    &
+                                add A    S1 S2 &
+                                add B    S2 S3 &
+                                remove X S3 S4 &
+                                remove Y S4 S5 &
+                                empty    S5)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r 1322ed8e0ee4 -r 5b1d47d920ce src/HOL/Prolog/Type.thy
--- a/src/HOL/Prolog/Type.thy	Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Type.thy	Wed Sep 07 21:07:09 2005 +0200
@@ -1,23 +1,24 @@
 (*  Title:    HOL/Prolog/Type.thy
     ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-type inference 
 *)
 
-Type = Func +
+header {* Type inference *}
 
-types ty
+theory Type
+imports Func
+begin
 
-arities ty :: type
+typedecl ty
 
-consts  bool	:: ty
-	nat	:: ty
-	"->"	:: ty => ty => ty	(infixr 20)
-	typeof	:: [tm, ty] => bool
-        anyterm :: tm
+consts
+  bool    :: ty
+  nat     :: ty
+  "->"    :: "ty => ty => ty"       (infixr 20)
+  typeof  :: "[tm, ty] => bool"
+  anyterm :: tm
 
-rules	common_typeof	"
+axioms  common_typeof:   "
 typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
 
 typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
@@ -35,13 +36,15 @@
 typeof (M - N) nat :- typeof M nat & typeof N nat..
 typeof (M * N) nat :- typeof M nat & typeof N nat"
 
-rules	good_typeof	"
+axioms good_typeof:     "
 typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
 
-rules	bad1_typeof	"
+axioms bad1_typeof:     "
 typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
 
-rules	bad2_typeof	"
+axioms bad2_typeof:     "
 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end