# HG changeset patch
# User paulson
# Date 906367434 -7200
# Node ID 3896c7894a57daf21b4303d1f24786ae8833b8b6
# Parent  4327eec06849107c408a36c1d224a819a3bc6695
Unary minus is now #- and not #~

diff -r 4327eec06849 -r 3896c7894a57 src/HOL/ex/BinEx.ML
--- a/src/HOL/ex/BinEx.ML	Mon Sep 21 10:43:09 1998 +0200
+++ b/src/HOL/ex/BinEx.ML	Mon Sep 21 10:43:54 1998 +0200
@@ -11,21 +11,21 @@
 by (Simp_tac 1);
 result();
 
-Goal "#1359  +  #~2468 = #~1109";
+Goal "#1359  +  #-2468 = #-1109";
 by (Simp_tac 1);
 result();
 
-Goal "#93746 +  #~46375 = #47371";
+Goal "#93746 +  #-46375 = #47371";
 by (Simp_tac 1);
 result();
 
 (** Negation **)
 
-Goal "- #65745 = #~65745";
+Goal "- #65745 = #-65745";
 by (Simp_tac 1);
 result();
 
-Goal "- #~54321 = #54321";
+Goal "- #-54321 = #54321";
 by (Simp_tac 1);
 result();
 
@@ -36,7 +36,7 @@
 by (Simp_tac 1);
 result();
 
-Goal "#~84  *  #51 = #~4284";
+Goal "#-84  *  #51 = #-4284";
 by (Simp_tac 1);
 result();
 
@@ -44,7 +44,7 @@
 by (Simp_tac 1);
 result();
 
-Goal "#1359  *  #~2468 = #~3354012";
+Goal "#1359  *  #-2468 = #-3354012";
 by (Simp_tac 1);
 result();
 
@@ -56,7 +56,7 @@
 by (Simp_tac 1); 
 result();
 
-Goal "#~345 < #~242 + #~100";  
+Goal "#-345 < #-242 + #-100";  
 by (Simp_tac 1); 
 result();
 
diff -r 4327eec06849 -r 3896c7894a57 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Sep 21 10:43:09 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 21 10:43:54 1998 +0200
@@ -94,7 +94,7 @@
 val scan_tid = $$ "'" ^^ scan_id;
 
 val scan_nat = scan_digits1 >> implode;
-val scan_int = $$ "~" ^^ scan_nat || scan_nat;
+val scan_int = $$ "-" ^^ scan_nat || scan_nat;
 
 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
 val scan_var = $$ "?" ^^ scan_id_nat;