--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Bin.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,42 @@
+(* Title: ZF/ex/bin.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Datatype of binary integers
+*)
+
+(*Example of a datatype with an infix constructor*)
+structure Bin = Datatype_Fun
+ (val thy = Univ.thy;
+ val rec_specs =
+ [("bin", "univ(0)",
+ [(["Plus", "Minus"], "i"),
+ (["op $$"], "[i,i]=>i")])];
+ val rec_styp = "i";
+ val ext = Some (NewSext {
+ mixfix =
+ [Infixl("$$", "[i,i] => i", 60)],
+ xrules = [],
+ parse_ast_translation = [],
+ parse_preproc = None,
+ parse_postproc = None,
+ parse_translation = [],
+ print_translation = [],
+ print_preproc = None,
+ print_postproc = None,
+ print_ast_translation = []});
+ val sintrs =
+ ["Plus : bin",
+ "Minus : bin",
+ "[| w: bin; b: bool |] ==> w$$b : bin"];
+ val monos = [];
+ val type_intrs = bool_into_univ::data_typechecks;
+ val type_elims = []);
+
+(*Perform induction on l, then prove the major premise using prems. *)
+fun bin_ind_tac a prems i =
+ EVERY [res_inst_tac [("x",a)] Bin.induct i,
+ rename_last_tac a ["1"] (i+3),
+ ares_tac prems i];
+