(void)
authorhaftmann
Tue Sep 19 15:22:03 2006 +0200 (2006-09-19)
changeset 205963950e65f48f8
parent 20595 db6bedfba498
child 20597 65fe827aa595
(void)
src/HOL/Integ/Numeral.thy
src/Pure/Pure.thy
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/HOL/Integ/Numeral.thy	Tue Sep 19 15:21:58 2006 +0200
     1.2 +++ b/src/HOL/Integ/Numeral.thy	Tue Sep 19 15:22:03 2006 +0200
     1.3 @@ -441,6 +441,7 @@
     1.4    by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
     1.5      Ints_odd_less_0 Ints_def split: bit.split)
     1.6  
     1.7 +
     1.8  text {* Less-Than or Equals *}
     1.9  
    1.10  text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
     2.1 --- a/src/Pure/Pure.thy	Tue Sep 19 15:21:58 2006 +0200
     2.2 +++ b/src/Pure/Pure.thy	Tue Sep 19 15:22:03 2006 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  
     2.5  setup  -- {* Common setup of internal components *}
     2.6  
     2.7 -
     2.8  subsection {* Meta-level connectives in assumptions *}
     2.9  
    2.10  lemma meta_mp:
     3.1 --- a/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:21:58 2006 +0200
     3.2 +++ b/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:22:03 2006 +0200
     3.3 @@ -88,9 +88,9 @@
     3.4    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
     3.5  
     3.6  fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
     3.7 -  |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
     3.8 -  |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
     3.9 -  |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    3.10 +  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
    3.11 +  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    3.12 +  | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    3.13  
    3.14  (*
    3.15     A typical operation, why functions might be good for, is