Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOLogic.dest_binum;
authorwenzelm
Fri, 12 Jan 2001 20:03:04 +0100
changeset 10890 0b4e916f51ed
parent 10889 aed0a0450797
child 10891 890b117f6189
HOLogic.dest_binum;
src/HOL/Integ/int_arith1.ML file | annotate | diff | comparison | revisions
src/HOL/Integ/nat_simprocs.ML file | annotate | diff | comparison | revisions
src/HOL/Real/RealBin.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/int_arith1.ML	Fri Jan 12 18:00:40 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Jan 12 20:03:04 2001 +0100
@@ -83,8 +83,8 @@
 
 (*Decodes a binary INTEGER*)
 fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+     (HOLogic.dest_binum w
+      handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
--- a/src/HOL/Integ/nat_simprocs.ML	Fri Jan 12 18:00:40 2001 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri Jan 12 20:03:04 2001 +0100
@@ -113,8 +113,8 @@
 fun dest_numeral (Const ("0", _)) = 0
   | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
   | dest_numeral (Const("Numeral.number_of", _) $ w) =
-      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
-       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
+      (BasisLibrary.Int.max (0, HOLogic.dest_binum w)
+       handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
--- a/src/HOL/Real/RealBin.ML	Fri Jan 12 18:00:40 2001 +0100
+++ b/src/HOL/Real/RealBin.ML	Fri Jan 12 20:03:04 2001 +0100
@@ -281,8 +281,8 @@
 
 (*Decodes a binary real constant*)
 fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Real_Numeral_Simprocs.dest_numeral:1", [w]))
+     (HOLogic.dest_binum w
+      handle TERM _ => raise TERM("Real_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t = raise TERM("Real_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
isabelle