aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-2/+1
* Proving path composition. Need to set up the Simplifier to simplify applicati...Josh Chen2018-06-301-0/+1
* Finished proofs of projectionsJosh Chen2018-06-301-1/+1
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-5/+13
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-12/+19
* Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen2018-06-171-1/+1
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-6/+13
* Reorganize codeJosh Chen2018-06-091-0/+48