# HG changeset patch
# User berghofe
# Date 1171387048 -3600
# Node ID 90694c1fa7146fea9e92cb8ecc5c83f929831610
# Parent  ebcd44cb8d618381e945f92f74ed84ca6f869d12
Added new file nominal_inductive.ML

diff -r ebcd44cb8d61 -r 90694c1fa714 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Feb 13 18:16:50 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Feb 13 18:17:28 2007 +0100
@@ -9,6 +9,7 @@
   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
   ("nominal_primrec.ML")
+  ("nominal_inductive.ML")
 begin 
 
 section {* Permutations *}
@@ -3020,6 +3021,9 @@
 (** primitive recursive functions on nominal datatypes **)
 use "nominal_primrec.ML"
 
+(** inductive predicates involving nominal datatypes **)
+use "nominal_inductive.ML"
+
 (*****************************************)
 (* setup for induction principles method *)