src/FOL/ex/.prolog.thy.ML

new Ring example

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