diff -r 000000000000 -r a5a9c433f639 src/FOL/ex/.prolog.thy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/.prolog.thy.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,55 @@
+structure Prolog =
+struct
+
+local
+ val parse_ast_translation = []
+ val parse_preproc = None
+ val parse_postproc = None
+ val parse_translation = []
+ val print_translation = []
+ val print_preproc = None
+ val print_postproc = None
+ val print_ast_translation = []
+in
+
+(**** begin of user section ****)
+
+(**** end of user section ****)
+
+val thy = extend_theory (FOL.thy)
+ "Prolog"
+ ([],
+  [],
+  [(["list"], 1)],
+  [(["list"], ([["term"]], "term"))],
+  [(["Nil"], "'a list"),
+   (["app"], "['a list, 'a list, 'a list] => o"),
+   (["rev"], "['a list, 'a list] => o")],
+  Some (NewSext {
+   mixfix =
+    [Infixr(":", "['a, 'a list]=> 'a list", 60)],
+   xrules =
+    [],
+   parse_ast_translation = parse_ast_translation,
+   parse_preproc = parse_preproc,
+   parse_postproc = parse_postproc,
+   parse_translation = parse_translation,
+   print_translation = print_translation,
+   print_preproc = print_preproc,
+   print_postproc = print_postproc,
+   print_ast_translation = print_ast_translation}))
+ [("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)")]
+
+val ax = get_axiom thy
+
+val appNil = ax "appNil"
+val appCons = ax "appCons"
+val revNil = ax "revNil"
+val revCons = ax "revCons"
+
+
+end
+end