src/HOL/Complex/NSInduct.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/NSInduct.thy	Mon May 05 18:22:31 2003 +0200
@@ -0,0 +1,23 @@
+(*  Title:       NSInduct.thy
+    Author:      Jacques D. Fleuriot
+    Copyright:   2001  University of Edinburgh
+    Description: Nonstandard characterization of induction etc.
+*)
+
+NSInduct =  ComplexArith0 + 
+
+constdefs
+
+  starPNat :: (nat => bool) => hypnat => bool  ("*pNat* _" [80] 80)
+  "*pNat* P == (%x. EX X. (X: Rep_hypnat(x) & 
+                      {n. P(X n)} : FreeUltrafilterNat))" 
+
+
+  starPNat2 :: (nat => nat => bool) => hypnat =>hypnat => bool  ("*pNat2* _" [80] 80)
+  "*pNat2* P == (%x y. EX X. EX Y. (X: Rep_hypnat(x) & Y: Rep_hypnat(y) & 
+                      {n. P(X n) (Y n)} : FreeUltrafilterNat))" 
+
+  hSuc :: hypnat => hypnat
+  "hSuc n == n + 1"
+    
+end
\ No newline at end of file