nominal2: Nominal/Perm.thy@0f24c961b5f6 (annotated)

1159 3c6bee89d826 Ported Stefan's permutation code, still needs some localizing. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Perm
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2163 diff changeset	2	imports
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2163 diff changeset	3	"../Nominal-General/Nominal2_Base"
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	4	"../Nominal-General/Nominal2_Atoms"
2302 c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2300 diff changeset	5	"../Nominal-General/Nominal2_Eqvt"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2300 diff changeset	6	"Nominal2_FSet"
c6db12ddb60c intermediate state Christian Urban <urbanc@in.tum.de> parents: 2300 diff changeset	7	"Abs"
2305 93ab397f5980 smaller code for raw-eqvt proofs Christian Urban <urbanc@in.tum.de> parents: 2302 diff changeset	8	uses ("nominal_dt_rawperm.ML")
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	9	("nominal_dt_rawfuns.ML")
2305 93ab397f5980 smaller code for raw-eqvt proofs Christian Urban <urbanc@in.tum.de> parents: 2302 diff changeset	10	("nominal_dt_alpha.ML")
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: 2335 diff changeset	11	("nominal_dt_quot.ML")
1159 3c6bee89d826 Ported Stefan's permutation code, still needs some localizing. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	begin
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	14	use "nominal_dt_rawperm.ML"
2297 9ca7b249760e tuned Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	15	ML {* open Nominal_Dt_RawPerm *}
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	16
2297 9ca7b249760e tuned Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	17	use "nominal_dt_rawfuns.ML"
9ca7b249760e tuned Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	18	ML {* open Nominal_Dt_RawFuns *}
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	19
2297 9ca7b249760e tuned Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	20	use "nominal_dt_alpha.ML"
9ca7b249760e tuned Christian Urban <urbanc@in.tum.de> parents: 2296 diff changeset	21	ML {* open Nominal_Dt_Alpha *}
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	22
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: 2335 diff changeset	23	use "nominal_dt_quot.ML"
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: 2335 diff changeset	24	ML {* open Nominal_Dt_Quot *}
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: 2335 diff changeset	25
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: 2335 diff changeset	26
1903 950fd9b8f05e reordered code Christian Urban <urbanc@in.tum.de> parents: 1902 diff changeset	27	end

author	Christian Urban <urbanc@in.tum.de>
	Sat, 31 Jul 2010 01:24:39 +0100
changeset 2389	0f24c961b5f6
parent 2346	4c5881455923
permissions	-rw-r--r--