Nominal/Parser.thy
2010-05-03 Cezary Kaliszyk remove tracing
2010-05-03 Cezary Kaliszyk Fix Parser
2010-05-02 Christian Urban moved old parser and old fv back into their original places; isabelle make works again
2010-04-30 Cezary Kaliszyk NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Cezary Kaliszyk Merged nominal_datatype into NewParser until eqvts
2010-04-30 Cezary Kaliszyk more parser/new parser synchronization.
2010-04-30 Cezary Kaliszyk Simplify old parser for integration
2010-04-25 Christian Urban tuned and made to compile
2010-04-24 Christian Urban merged
2010-04-21 Christian Urban merged
2010-04-20 Christian Urban renamed Ex1.thy to SingleLet.thy
2010-04-20 Cezary Kaliszyk Fix of comment
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Locations of files in Parser
2010-04-14 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
2010-04-11 Christian Urban tuned
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk Parsing of list-bn functions into components.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-25 Cezary Kaliszyk Proper bn_rsp, for bn functions calling each other.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
less more (0) -100 -50 -30 tip