--- a/src/FOL/ex/Prolog.thy Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/Prolog.thy Sat Sep 03 17:15:51 2005 +0200
@@ -2,21 +2,27 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-First-Order Logic: PROLOG examples
-
-Inherits from FOL the class term, the type o, and the coercion Trueprop
*)
-Prolog = FOL +
-types 'a list
-arities list :: (term)term
-consts Nil :: 'a list
- ":" :: ['a, 'a list]=> 'a list (infixr 60)
- app :: ['a list, 'a list, 'a list] => o
- rev :: ['a list, 'a list] => o
-rules appNil "app(Nil,ys,ys)"
- appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
- revNil "rev(Nil,Nil)"
- revCons "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
+header {* First-Order Logic: PROLOG examples *}
+
+theory Prolog
+imports FOL
+begin
+
+typedecl 'a list
+arities list :: ("term") "term"
+consts
+ Nil :: "'a list"
+ Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60)
+ app :: "['a list, 'a list, 'a list] => o"
+ rev :: "['a list, 'a list] => o"
+axioms
+ appNil: "app(Nil,ys,ys)"
+ appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
+ revNil: "rev(Nil,Nil)"
+ revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end