src/Tools/8bit/isa-patches/HOL/HOL2.p

Goal: tuned pris;

local open Ast;
fun Gbigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
      fold_ast_p "êë" (unfold_ast "_asms" asms, concl)
  | Gbigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
fun Glam_ast_tr (*"Glam"*) [idts, body] =
      fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
  | Glam_ast_tr (*"Glam"*) asts = raise_ast "lambda_ast_tr" asts;

fun Gimpl_ast_tr' (*"Gbigimpl"*) asts =
  (case unfold_ast_p "êë" (Appl (Constant "êë" :: asts)) of
    (asms as _ :: _ :: _, concl)
      => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
  | _ => raise Match);
in
    val parse_ast_translation = ("Gbigimpl", Gbigimpl_ast_tr)::
				("Glam", Glam_ast_tr)::
				parse_ast_translation;

    val print_ast_translation = ("êë", Gimpl_ast_tr')::
				("_lambda", fn asts => 
					Appl (Constant "Glam" :: asts)) ::	
				print_ast_translation;

end;

local open Syntax in
val thy = thy 
|> add_trrules_i 
[mk_appl (Constant "Ú" ) [Variable "P", Variable "Q"] <-> 
 mk_appl (Constant "==") [Variable "P", Variable "Q"],
 mk_appl (Constant "êë" ) [Variable "P", Variable "Q"] <-> 
 mk_appl (Constant "==>") [Variable "P", Variable "Q"],
 (Constant "Ä" ) <->  (Constant "!!")]
end;