--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/prolog.thy Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,22 @@
+(* Title: FOL/ex/prolog.thy
+ 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 list 1
+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)"
+end