src/HOL/Integ/int_factor_simprocs.ML
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 11868 56db9f3a6b3e
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -114,33 +114,33 @@
     1.4  set trace_simp;
     1.5  fun test s = (Goal s; by (Simp_tac 1)); 
     1.6  
     1.7 -test "# 9*x = # 12 * (y::int)";
     1.8 -test "(# 9*x) div (# 12 * (y::int)) = z";
     1.9 -test "# 9*x < # 12 * (y::int)";
    1.10 -test "# 9*x <= # 12 * (y::int)";
    1.11 +test "9*x = 12 * (y::int)";
    1.12 +test "(9*x) div (12 * (y::int)) = z";
    1.13 +test "9*x < 12 * (y::int)";
    1.14 +test "9*x <= 12 * (y::int)";
    1.15  
    1.16 -test "# -99*x = # 132 * (y::int)";
    1.17 -test "(# -99*x) div (# 132 * (y::int)) = z";
    1.18 -test "# -99*x < # 132 * (y::int)";
    1.19 -test "# -99*x <= # 132 * (y::int)";
    1.20 +test "-99*x = 132 * (y::int)";
    1.21 +test "(-99*x) div (132 * (y::int)) = z";
    1.22 +test "-99*x < 132 * (y::int)";
    1.23 +test "-99*x <= 132 * (y::int)";
    1.24  
    1.25 -test "# 999*x = # -396 * (y::int)";
    1.26 -test "(# 999*x) div (# -396 * (y::int)) = z";
    1.27 -test "# 999*x < # -396 * (y::int)";
    1.28 -test "# 999*x <= # -396 * (y::int)";
    1.29 +test "999*x = -396 * (y::int)";
    1.30 +test "(999*x) div (-396 * (y::int)) = z";
    1.31 +test "999*x < -396 * (y::int)";
    1.32 +test "999*x <= -396 * (y::int)";
    1.33  
    1.34 -test "# -99*x = # -81 * (y::int)";
    1.35 -test "(# -99*x) div (# -81 * (y::int)) = z";
    1.36 -test "# -99*x <= # -81 * (y::int)";
    1.37 -test "# -99*x < # -81 * (y::int)";
    1.38 +test "-99*x = -81 * (y::int)";
    1.39 +test "(-99*x) div (-81 * (y::int)) = z";
    1.40 +test "-99*x <= -81 * (y::int)";
    1.41 +test "-99*x < -81 * (y::int)";
    1.42  
    1.43 -test "# -2 * x = # -1 * (y::int)";
    1.44 -test "# -2 * x = -(y::int)";
    1.45 -test "(# -2 * x) div (# -1 * (y::int)) = z";
    1.46 -test "# -2 * x < -(y::int)";
    1.47 -test "# -2 * x <= # -1 * (y::int)";
    1.48 -test "-x < # -23 * (y::int)";
    1.49 -test "-x <= # -23 * (y::int)";
    1.50 +test "-2 * x = -1 * (y::int)";
    1.51 +test "-2 * x = -(y::int)";
    1.52 +test "(-2 * x) div (-1 * (y::int)) = z";
    1.53 +test "-2 * x < -(y::int)";
    1.54 +test "-2 * x <= -1 * (y::int)";
    1.55 +test "-x < -23 * (y::int)";
    1.56 +test "-x <= -23 * (y::int)";
    1.57  *)
    1.58  
    1.59