Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
authorberghofe
Fri, 28 Apr 2006 17:56:20 +0200
changeset 19499 1a082c1257d7
parent 19498 7dcf9903eeb3
child 19500 188d4e44c1a6
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
src/HOL/IsaMakefile
src/HOL/Nominal/Examples/ROOT.ML
--- 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
--- 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";