# HG changeset patch
# User wenzelm
# Date 1343159208 -7200
# Node ID e06ea2327cc5aeb2dd90fc862ca8f22fbede5461
# Parent  94a9650f79fb450e8dab1c8d7398b67b99a2c2db
reactivated HOL-NSA-Examples;

diff -r 94a9650f79fb -r e06ea2327cc5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 24 21:36:53 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 24 21:46:48 2012 +0200
@@ -57,6 +57,7 @@
   HOL-Mutabelle \
   HOL-NanoJava \
   HOL-Nitpick_Examples \
+  HOL-NSA-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Quotient_Examples \
diff -r 94a9650f79fb -r e06ea2327cc5 src/HOL/NSA/Examples/NSPrimes.thy
--- a/src/HOL/NSA/Examples/NSPrimes.thy	Tue Jul 24 21:36:53 2012 +0200
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Tue Jul 24 21:46:48 2012 +0200
@@ -23,10 +23,10 @@
   choicefun :: "'a set => 'a" where
   "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
 
-consts injf_max :: "nat => ('a::{order} set) => 'a"
-primrec
+primrec injf_max :: "nat => ('a::{order} set) => 'a"
+where
   injf_max_zero: "injf_max 0 E = choicefun E"
-  injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
+| injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
 
 
 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"