equal
deleted
inserted
replaced
81 |
81 |
82 fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n; |
82 fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n; |
83 |
83 |
84 (*Decodes a binary INTEGER*) |
84 (*Decodes a binary INTEGER*) |
85 fun dest_numeral (Const("Numeral.number_of", _) $ w) = |
85 fun dest_numeral (Const("Numeral.number_of", _) $ w) = |
86 (NumeralSyntax.dest_bin w |
86 (HOLogic.dest_binum w |
87 handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) |
87 handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) |
88 | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); |
88 | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); |
89 |
89 |
90 fun find_first_numeral past (t::terms) = |
90 fun find_first_numeral past (t::terms) = |
91 ((dest_numeral t, rev past @ terms) |
91 ((dest_numeral t, rev past @ terms) |
92 handle TERM _ => find_first_numeral (t::past) terms) |
92 handle TERM _ => find_first_numeral (t::past) terms) |