darcs-mirror-isa-launchbury.git
2015-02-03 Joachim BreitnerAdd a drop rule to SestoftGC master
2015-01-28 Joachim BreitnerFix end-to-end proof to finally obtain the unmodified...
2015-01-27 Joachim BreitnerRemove some dead code
2015-01-26 Joachim BreitnerCorrectness via card, ugly proof from GCstep to step...
2015-01-20 Joachim BreitnerNo need for heap_upds_ok in EtaExpandCorrect
2015-01-20 Joachim BreitnerSeparate Arity consistency from Cardinality consistency
2015-01-16 Joachim BreitnerFinish CardinalityetaExpandCorrect with IfThenElse
2015-01-16 Joachim BreitnerSwitch to Bool b; prepare CardinalityetaExpandCorrect...
2015-01-16 Joachim BreitnerPrepare CardinalityEtaExpand for a stack with expressions
2015-01-15 Joachim BreitnerUse isVal everywhere
2015-01-15 Joachim BreitnerAdd Null and (e ? e : e)
2015-01-15 Joachim BreitnerGet rid of GVar detour
2015-01-15 Joachim BreitnerForgotten theory before-adding-ifthenelse
2015-01-15 Joachim BreitnerAdd forgotten ArityEtaExpand
2015-01-15 Joachim BreitnerMore module splitting
2015-01-14 Joachim BreitnerAvoid theory-level interpretation
2015-01-14 Joachim BreitnerSplit CoCallCardinality into CoCall* modules
2015-01-14 Joachim BreitnerModules FTreeAnalysisSig, FTreeAnalysisSpec
2015-01-14 Joachim BreitnerUnused import
2015-01-14 Joachim BreitnerModule name: CoCallAnalysisSig
2015-01-14 Joachim BreitnerGet rid of ccExp'
2015-01-14 Joachim BreitnerGet rid of Aexp'
2015-01-14 Joachim BreitnerSome module reorganization
2015-01-13 Joachim BreitnerUnused locale
2015-01-13 Joachim BreitnerRemove more commented code
2015-01-13 Joachim BreitnerRemove some commented code
2015-01-12 Joachim BreitnerExample end-to-end transformation
2015-01-12 Joachim BreitnerChange parameter of ccNeighbors to a variable
2015-01-09 Joachim BreitnerAexp_restr_subst and CCexp_subst mutual recursive....
2015-01-09 Joachim BreitnerAexp_subst_upd can be derived from Aexp_subst, move...
2015-01-09 Joachim BreitnerLess aggressive ccBindsExtra
2015-01-09 Joachim BreitnerMake use of wild_recursion_thunked
2015-01-08 Joachim BreitnerPartial work adding nonrecursive bindings as well;...
2015-01-08 Joachim BreitnerAdd a wild_recursion variant that caters for thunks
2015-01-08 Joachim BreitnerMake wild_recursion weaker
2015-01-07 Joachim BreitnerAdd non-rec case to the implementation
2015-01-07 Joachim BreitnerBack to edom ae = edom ce
2015-01-07 Joachim BreitnerFix NoCardinalityAnalysis.thy a bit, but still broken
2015-01-07 Joachim BreitnerEnd-to-end theory for sanity checking
2015-01-07 Joachim BreitnerDefine non-recursive bindings
2015-01-05 Joachim BreitnerAllow ae and ce to differ in their domain. Ugly, but...
2015-01-05 Joachim BreitnerExtract FTreeAnalysis
2014-12-19 Joachim BreitnerDemand more in FutureAnalysisCarrier
2014-12-19 Joachim BreitnerFix indentation
2014-12-19 Joachim BreitnerMore lemmas moved
2014-12-19 Joachim BreitnerMake Tex more robust
2014-12-19 Joachim BreitnerLots of cleanup
2014-12-17 Joachim BreitnerSorry-Frei! (Fehlt noch: Nicht-rekursive Lets, und...
2014-12-16 Joachim BreitnerMake CoCallAnalyis use Afix from ArityAnalysis
2014-12-16 Joachim BreitnerFix some sorries
2014-12-16 Joachim BreitnerAfix does not have to take CoCallGraph into account
2014-12-15 Joachim Breitneredom_Afix
2014-12-15 Joachim BreitnerLooks like no special treatment for linear recursion...
2014-12-12 Joachim BreitnerccFTree_below_singleI, paths_withoutI
2014-12-11 Joachim BreitnerLarge unsorted commit. Special casing for linear recurs...
2014-12-03 Joachim BreitnerAdd join_comm, join_assoc to simpset. Hopefully helpful...
2014-12-01 Joachim BreitnerAdjust CardinalityEtaExpand and FTreeCardinatly to...
2014-11-26 Joachim BreitnerSchadensbegrenzung. substitute mit extra "thunks" Parameter
2014-11-26 Joachim BreitnerTowards Let, but stuck: stubstitute needs to cater...
2014-11-25 Joachim BreitnerNon-Let-parts of CoCalls-to-ftree Conversation
2014-11-21 Joachim BreitnerCleanup
2014-11-21 Joachim BreitnerFactor out AnalBinds
2014-11-21 Joachim BreitnerDisjointness lemmas in FTreeCardinality
2014-11-20 Joachim BreitnerContinuity of substitute, both
2014-11-20 Joachim BreitnerNice syntax for either
2014-11-20 Joachim BreitnerNice syntax for both
2014-11-20 Joachim BreitnerReorder lemmas in FTree
2014-11-19 Joachim BreitnerYay for force
2014-11-19 Joachim BreitnerNew file List-Interleavings
2014-11-18 Joachim BreitnerHuge proofs for ftree_restr_both and ftree_rest_substitute
2014-11-17 Joachim BreitnerPlan for CardinalityPrognosisCorrectLet
2014-11-17 Joachim BreitnerAvoid talking about substitute'
2014-11-17 Joachim BreitnerCardinalityPrognosisCorrect fertig
2014-11-14 Joachim BreitnerMore progress on variables rules in various variants
2014-11-14 Joachim BreitnerFrom ftree to cardinality
2014-11-14 Joachim BreitnerStuff in FutureCardinality.thy
2014-11-14 Joachim BreitnerLess assumptions passed to prognosis_Var
2014-11-14 Joachim BreitnerType of infinite trees as down-ward-closed sets of...
2014-11-11 Joachim BreitnerBridge from Cardinality Analysis to Prognosis based...
2014-11-10 Joachim BreitnerRemove unused Arity Correctness locales
2014-11-10 Joachim BreitnerUse FutureEtaExpand proof also in ArityEtaExpand proof
2014-11-06 Joachim BreitnerFound a sorry...
2014-11-06 Joachim BreitnerAdding a trivial cardinality analysis to an arity analysis
2014-11-06 Joachim Breitners/fHeap/cHeap/g
2014-11-06 Joachim BreitnerClean out FutureEtaExpand
2014-11-05 Joachim BreitnerAll sorries moved to assumptions
2014-11-05 Joachim BreitnerGet rid of aSummary
2014-11-05 Joachim BreitnerRephrase stuff in terms of aSummary
2014-11-05 Joachim BreitnerMake aBinds nicer
2014-11-05 Joachim BreitnerStuff...
2014-11-04 Joachim BreitnerSimplify aHeap and fHeap
2014-11-04 Joachim BreitnerMore stuff in FutureEtaExpand
2014-11-03 Joachim BreitnerThe frame for the proof for let
2014-10-31 Joachim BreitnerMore work on that, but now stuck: Again information...
2014-10-31 Joachim BreitnerProgress towards a correctness proof based on futures
2014-10-24 Joachim BreitnerBeginnings of CallArityEtaExpand.thy
2014-10-24 Joachim BreitnerSlightly more general AbstractTransform
2014-10-23 Joachim BreitnerDefine ccExp
2014-10-22 Joachim BreitnerRahmem für die CC-Analyse
2014-10-22 Joachim BreitnerMore complete trivial Arity Analysis
next