--- 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. *}
--- 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:
--- 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