Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
--- 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";