nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -300 -100 -60 +60 +100 +300 +1000 tip

applic_prs
2009-11-25, by Cezary Kaliszyk
polishing
2009-11-25, by Christian Urban
reordered the code
2009-11-25, by Christian Urban
Moved exception handling to QuotMain and cleaned FSet.
2009-11-25, by Cezary Kaliszyk
Merge
2009-11-25, by Cezary Kaliszyk
Finished manual lifting of list_induct_part :)
2009-11-25, by Cezary Kaliszyk
comments tuning and slight reordering
2009-11-25, by Christian Urban
Merge
2009-11-25, by Cezary Kaliszyk
More moving from QuotMain to UnusedQuotMain
2009-11-25, by Cezary Kaliszyk
deleted some obsolete diagnostic code
2009-11-25, by Christian Urban
Removed unused things from QuotMain.
2009-11-25, by Cezary Kaliszyk
All examples work again.
2009-11-25, by Cezary Kaliszyk
cleaning in MyInt
2009-11-25, by Cezary Kaliszyk
lambda_prs and cleaning the existing examples.
2009-11-25, by Cezary Kaliszyk
merged
2009-11-25, by Christian Urban
fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-25, by Christian Urban
Ho-matching failures...
2009-11-24, by Cezary Kaliszyk
changed unification to matching
2009-11-24, by Christian Urban
unification
2009-11-24, by Christian Urban
Lambda & SOLVED' for new quotient_tac
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
Conversion
2009-11-24, by Cezary Kaliszyk
The non-working procedure_tac.
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
use error instead of raising our own exception
2009-11-24, by Christian Urban
Fixes to the tactic after quotient_tac changed.
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
added a prepare_tac
2009-11-24, by Christian Urban
TRY' for clean_tac
2009-11-24, by Cezary Kaliszyk
Moved cleaning to QuotMain
2009-11-24, by Cezary Kaliszyk
New cleaning tactic
2009-11-24, by Cezary Kaliszyk
explicit phases for the cleaning
2009-11-24, by Christian Urban
Separate regularize_tac
2009-11-24, by Cezary Kaliszyk
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
2009-11-24, by Cezary Kaliszyk
More fixes for inj_REPABS
2009-11-24, by Cezary Kaliszyk
addded a tactic, which sets up the three goals of the `algorithm'
2009-11-24, by Christian Urban
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
2009-11-23, by Christian Urban
merged
2009-11-23, by Christian Urban
tuned some comments
2009-11-23, by Christian Urban
Another not-typechecking regularized term.
2009-11-23, by Cezary Kaliszyk
domain_type in regularizing equality
2009-11-23, by Cezary Kaliszyk
More theorems lifted in the goal-directed way.
2009-11-23, by Cezary Kaliszyk
Finished temporary goal-directed lift_theorem wrapper.
2009-11-23, by Cezary Kaliszyk
merged
2009-11-23, by Christian Urban
a version of inj_REPABS (needs to be looked at again later)
2009-11-23, by Christian Urban
Fixes for atomize
2009-11-23, by Cezary Kaliszyk
merge
2009-11-23, by Cezary Kaliszyk
lift_thm with a goal.
2009-11-23, by Cezary Kaliszyk
slight change in code layout
2009-11-23, by Christian Urban
Fixes for new code
2009-11-23, by Cezary Kaliszyk
Removing dead code
2009-11-23, by Cezary Kaliszyk
Move atomize_goal to QuotMain
2009-11-23, by Cezary Kaliszyk
Removed second implementation of Regularize/Inject from FSet.
2009-11-23, by Cezary Kaliszyk
Moved new repabs_inj code to QuotMain
2009-11-23, by Cezary Kaliszyk
New repabs behaves the same way as old one.
2009-11-23, by Cezary Kaliszyk
code review with Cezary
2009-11-23, by Christian Urban
The other branch does not seem to work...
2009-11-23, by Cezary Kaliszyk
Fixes for recent changes.
2009-11-23, by Cezary Kaliszyk
updated to Isabelle 22nd November
2009-11-22, by Christian Urban
a little tuning of comments
2009-11-22, by Christian Urban

less more | (0) -300 -100 -60 +60 +100 +300 +1000 tip

nominal2