# HG changeset patch
# User berghofe
# Date 1146239780 -7200
# Node ID 1a082c1257d7b719b18fb002ed4be517356a5efb
# Parent  7dcf9903eeb35ed4359ee7a32e4c0bfb32883b46
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.

diff -r 7dcf9903eeb3 -r 1a082c1257d7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 28 16:04:57 2006 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 28 17:56:20 2006 +0200
@@ -741,7 +741,8 @@
 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
 
 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
-  Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy 				\
+  Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
+  Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy			\
   Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\
   Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy			\
   Nominal/Examples/Weakening.thy
diff -r 7dcf9903eeb3 -r 1a082c1257d7 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 28 16:04:57 2006 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 28 17:56:20 2006 +0200
@@ -6,6 +6,9 @@
 *)
 
 use_thy "CR";
-use_thy "SN";
+use_thy "Class";
+setmp quick_and_dirty true use_thy "Fsub"; (* FIXME *)
+use_thy "Lambda_mu";
 use_thy "Recursion";
+use_thy "SN";
 use_thy "Weakening";