nominal2: ROOT@c4f31f1564b7 (annotated)

3198 e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	1	session Nominal2 in "Nominal" = HOL +
3194 6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	options [document = false]
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	theories
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	"Nominal2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	"Atoms"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	"Eqvt"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	7
3198 e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	8	session Examples (Tests) in "Nominal" = Nominal2 +
3194 6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	options [document = false]
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	theories
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	"Ex/Weakening"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"Ex/Classical"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	"Ex/Datatypes"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	"Ex/Ex1"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	"Ex/ExPS3"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	"Ex/Multi_Recs"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	"Ex/Multi_Recs2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	"Ex/LF"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	"Ex/Lambda"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	("Ex/Let",)
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	"Ex/LetPat"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	"Ex/LetRec"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	"Ex/LetRec2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	"Ex/LetFun"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	"Ex/Modules"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	"Ex/SingleLet"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	"Ex/Shallow"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	"Ex/SystemFOmega"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	"Ex/TypeSchemes1"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	"Ex/TypeSchemes2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	"Ex/TypeVarsTest"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	"Ex/Foo1"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	"Ex/Foo2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	"Ex/CoreHaskell"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	"Ex/CoreHaskell2"
6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	"Ex/Pi"
3217 d67a6a48f1c7 added example for locales (by Tjark Weber) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3198 diff changeset	37	"Ex/Local_Contexts"
3196 ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	38	theories [quick_and_dirty]
ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	39	"Ex/Let"
3194 6454435d689b added new ROOT session file Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
3198 e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	41	session Tutorial_Exercises (Tests) in "Tutorial" = Nominal2 +
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	42	options [document = false, quick_and_dirty]
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	43	theories
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	44	"Lambda"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	45	"Minimal"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	46	"Tutorial1s"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	47	"Tutorial3s"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	48	"Tutorial4s"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	49	"Tutorial1"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	50	"Tutorial2"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	51	"Tutorial2s"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	52	"Tutorial3"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	53	"Tutorial4"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	54	"Tutorial5"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	55	"Tutorial6"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	56
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	57	session CPS (Tests) in "Nominal" = Nominal2 +
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	58	options [document = false, quick_and_dirty]
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	59	theories
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	60	"Ex/CPS/Lt"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	61	"Ex/CPS/CPS1_Plotkin"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	62	"Ex/CPS/CPS2_DanvyNielsen"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	63	"Ex/CPS/CPS3_DanvyFilinski"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	64	"Ex/CPS/CPS3_DanvyFilinski_FCB2"
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	65
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	66
e42d281bf5ef added a nefangled ROOT file Christian Urban <urbanc@in.tum.de> parents: 3196 diff changeset	67	session Esop in "ESOP-Paper" = Nominal2 +
3196 ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	68	theories [document = false]
ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	69	"~~/src/HOL/Library/LaTeXsugar"
ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	70	theories
ca6ca6fc28af tuned Christian Urban <urbanc@in.tum.de> parents: 3194 diff changeset	71	"Paper"
3224 cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	72	files "document/root.bib" "document/root.tex"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	73
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	74	session Slides1 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	75	options [document = pdf, document_output= "..", document_variants = "slides1"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	76	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	77	"Slides1"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	78
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	79	session Slides2 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	80	options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides2"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	81	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	82	"Slides2"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	83
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	84	session Slides3 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	85	options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides3"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	86	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	87	"Slides3"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	88
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	89	session Slides4 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	90	options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides4"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	91	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	92	"Slides4"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	93
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	94	session Slides5 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	95	options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides5"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	96	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	97	"Slides5"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	98
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	99	session Slides9 in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	100	options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides9"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	101	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	102	"Slides9"
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	103
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	104	session SlidesB in "Slides" = Nominal2 +
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	105	options [document = pdf, document_output= "..", document_variants = "slidesb"]
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	106	theories
cf451e182bf0 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3217 diff changeset	107	"SlidesB"

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sat, 19 Mar 2016 21:06:48 +0000 (2016-03-19)
branch	Nominal2-Isabelle2016
changeset 3243	c4f31f1564b7
parent 3224	cf451e182bf0
permissions	-rw-r--r--