/Nominal/
drwxr-xr-x [up]
drwxr-xr-x Ex
drwxr-xr-x Manual
-rw-r--r-- 2011-08-19 11:07 +0900 5697 Atoms.thy
-rw-r--r-- 2011-08-19 11:07 +0900 2045 Eqvt.thy
-rw-r--r-- 2011-08-19 11:07 +0900 25333 Nominal2.thy
-rw-r--r-- 2011-08-19 11:07 +0900 45447 Nominal2_Abs.thy
-rw-r--r-- 2011-08-19 11:07 +0900 96121 Nominal2_Base.thy
-rw-r--r-- 2011-08-19 11:07 +0900 16883 Nominal2_FCB.thy
-rw-r--r-- 2011-08-19 11:07 +0900 604 ROOT.ML
-rw-r--r-- 2011-08-19 11:07 +0900 3195 nominal_atoms.ML
-rw-r--r-- 2011-08-19 11:07 +0900 4788 nominal_basics.ML
-rw-r--r-- 2011-08-19 11:07 +0900 30205 nominal_dt_alpha.ML
-rw-r--r-- 2011-08-19 11:07 +0900 4958 nominal_dt_data.ML
-rw-r--r-- 2011-08-19 11:07 +0900 23957 nominal_dt_quot.ML
-rw-r--r-- 2011-08-19 11:07 +0900 17587 nominal_dt_rawfuns.ML
-rw-r--r-- 2011-08-19 11:07 +0900 4427 nominal_eqvt.ML
-rw-r--r-- 2011-08-19 11:07 +0900 10228 nominal_function.ML
-rw-r--r-- 2011-08-19 11:07 +0900 5058 nominal_function_common.ML
-rw-r--r-- 2011-08-19 11:07 +0900 37863 nominal_function_core.ML
-rw-r--r-- 2011-08-19 11:07 +0900 6623 nominal_induct.ML
-rw-r--r-- 2011-08-19 11:07 +0900 15159 nominal_inductive.ML
-rw-r--r-- 2011-08-19 11:07 +0900 16046 nominal_library.ML
-rw-r--r-- 2011-08-19 11:07 +0900 13363 nominal_mutual.ML
-rw-r--r-- 2011-08-19 11:07 +0900 7433 nominal_permeq.ML
-rw-r--r-- 2011-08-19 11:07 +0900 4106 nominal_termination.ML
-rw-r--r-- 2011-08-19 11:07 +0900 8020 nominal_thmdecls.ML