/Nominal/
drwxr-xr-x [up]
drwxr-xr-x Ex
drwxr-xr-x Manual
-rw-r--r-- 2013-03-11 16:37 +0000 5708 Atoms.thy
-rw-r--r-- 2013-03-11 16:37 +0000 2045 Eqvt.thy
-rw-r--r-- 2013-03-11 16:37 +0000 72 FROOT.ML
-rw-r--r-- 2013-03-11 16:37 +0000 17088 GPerm.thy
-rw-r--r-- 2013-03-11 16:37 +0000 25612 Nominal2.thy
-rw-r--r-- 2013-03-11 16:37 +0000 50202 Nominal2_Abs.thy
-rw-r--r-- 2013-03-11 16:37 +0000 105888 Nominal2_Base.thy
-rw-r--r-- 2013-03-11 16:37 +0000 103591 Nominal2_Base_Exec.thy
-rw-r--r-- 2013-03-11 16:37 +0000 18471 Nominal2_FCB.thy
-rw-r--r-- 2013-03-11 16:37 +0000 604 ROOT.ML
-rw-r--r-- 2013-03-11 16:37 +0000 3156 nominal_atoms.ML
-rw-r--r-- 2013-03-11 16:37 +0000 4795 nominal_basics.ML
-rw-r--r-- 2013-03-11 16:37 +0000 30251 nominal_dt_alpha.ML
-rw-r--r-- 2013-03-11 16:37 +0000 4577 nominal_dt_data.ML
-rw-r--r-- 2013-03-11 16:37 +0000 24858 nominal_dt_quot.ML
-rw-r--r-- 2013-03-11 16:37 +0000 17574 nominal_dt_rawfuns.ML
-rw-r--r-- 2013-03-11 16:37 +0000 4194 nominal_eqvt.ML
-rw-r--r-- 2013-03-11 16:37 +0000 10290 nominal_function.ML
-rw-r--r-- 2013-03-11 16:37 +0000 5092 nominal_function_common.ML
-rw-r--r-- 2013-03-11 16:37 +0000 38124 nominal_function_core.ML
-rw-r--r-- 2013-03-11 16:37 +0000 6635 nominal_induct.ML
-rw-r--r-- 2013-03-11 16:37 +0000 15130 nominal_inductive.ML
-rw-r--r-- 2013-03-11 16:37 +0000 16371 nominal_library.ML
-rw-r--r-- 2013-03-11 16:37 +0000 16933 nominal_mutual.ML
-rw-r--r-- 2013-03-11 16:37 +0000 7488 nominal_permeq.ML
-rw-r--r-- 2013-03-11 16:37 +0000 4343 nominal_termination.ML
-rw-r--r-- 2013-03-11 16:37 +0000 8023 nominal_thmdecls.ML