# HG changeset patch
# User haftmann
# Date 1158672123 -7200
# Node ID 3950e65f48f89c9ccfff6d49c582077ced460891
# Parent  db6bedfba49828a834b21b093de745b0d1997901
(void)

diff -r db6bedfba498 -r 3950e65f48f8 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Tue Sep 19 15:21:58 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy	Tue Sep 19 15:22:03 2006 +0200
@@ -441,6 +441,7 @@
   by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
     Ints_odd_less_0 Ints_def split: bit.split)
 
+
 text {* Less-Than or Equals *}
 
 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
diff -r db6bedfba498 -r 3950e65f48f8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Sep 19 15:21:58 2006 +0200
+++ b/src/Pure/Pure.thy	Tue Sep 19 15:22:03 2006 +0200
@@ -10,7 +10,6 @@
 
 setup  -- {* Common setup of internal components *}
 
-
 subsection {* Meta-level connectives in assumptions *}
 
 lemma meta_mp:
diff -r db6bedfba498 -r 3950e65f48f8 src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:21:58 2006 +0200
+++ b/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:22:03 2006 +0200
@@ -88,9 +88,9 @@
   | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
 
 fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
-  |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
-  |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
-  |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
+  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
+  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
+  | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
 
 (*
    A typical operation, why functions might be good for, is