Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-240
+240
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged
2009-12-04, by Christian Urban
not yet quite functional treatment of constants
2009-12-04, by Christian Urban
Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
2009-12-04, by Cezary Kaliszyk
Changing FOCUS to CSUBGOAL (part 1)
2009-12-04, by Cezary Kaliszyk
abs_rep as ==
2009-12-04, by Cezary Kaliszyk
Cleaning the Quotients file
2009-12-04, by Cezary Kaliszyk
Minor renames and moving
2009-12-04, by Cezary Kaliszyk
Cleaning/review of QuotScript.
2009-12-04, by Cezary Kaliszyk
More cleaning
2009-12-04, by Cezary Kaliszyk
more name cleaning and removing
2009-12-04, by Cezary Kaliszyk
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning & Renaming coming from QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning in Quotients
2009-12-04, by Cezary Kaliszyk
Even more name changes and cleaning
2009-12-04, by Cezary Kaliszyk
More code cleaning and name changes
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Cezary Kaliszyk
smaller theory footprint
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
merge
2009-12-04, by Christian Urban
smaller theory footprint
2009-12-04, by Christian Urban
More name changes
2009-12-04, by Cezary Kaliszyk
Naming changes
2009-12-04, by Cezary Kaliszyk
code cleaning and renaming
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Removed previous inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
some tuning
2009-12-04, by Christian Urban
merge
2009-12-04, by Cezary Kaliszyk
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04, by Cezary Kaliszyk
compose_tac instead of rtac to avoid unification; some code cleaning.
2009-12-04, by Cezary Kaliszyk
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
2009-12-04, by Cezary Kaliszyk
Using APPLY_RSP1; again a little bit faster.
2009-12-04, by Cezary Kaliszyk
Fixes after big merge.
2009-12-04, by Cezary Kaliszyk
The big merge; probably non-functional.
2009-12-04, by Cezary Kaliszyk
Testing the new tactic everywhere
2009-12-04, by Cezary Kaliszyk
First version of the deterministic rep-abs-inj-tac.
2009-12-04, by Cezary Kaliszyk
Changing = to \<equiv> in case if we want to use simp.
2009-12-04, by Cezary Kaliszyk
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Made your version work again with LIST_REL_EQ.
2009-12-04, by Cezary Kaliszyk
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03, by Christian Urban
removed quot argument...not all examples work anymore
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
first version of internalised quotient theorems; added FIXME-TODO
2009-12-03, by Christian Urban
further dead code
2009-12-03, by Christian Urban
Reintroduced varifyT; we still need it for permutation definition.
2009-12-03, by Cezary Kaliszyk
Updated the examples
2009-12-03, by Cezary Kaliszyk
Fixed previous mistake
2009-12-03, by Cezary Kaliszyk
defs used automatically by clean_tac
2009-12-03, by Cezary Kaliszyk
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
2009-12-03, by Cezary Kaliszyk
Added the definition to quotient constant data.
2009-12-03, by Cezary Kaliszyk
removing unused code
2009-12-03, by Cezary Kaliszyk
merged
2009-12-03, by Christian Urban
deleted some dead code
2009-12-03, by Christian Urban
Included all_prs and ex_prs in the lambda_prs conversion.
2009-12-03, by Cezary Kaliszyk
further simplification
2009-12-03, by Christian Urban
simplified lambda_prs_conv
2009-12-03, by Christian Urban
deleted now obsolete argument rty everywhere
2009-12-02, by Christian Urban
deleted tests at the beginning of QuotMain
2009-12-02, by Christian Urban
Experiments with OPTION_map
2009-12-02, by Cezary Kaliszyk
merge
2009-12-02, by Cezary Kaliszyk
More experiments with higher order quotients and theorems with non-lifted constants.
2009-12-02, by Cezary Kaliszyk
merged
2009-12-02, by Christian Urban
Lifting to 2 different types :)
2009-12-02, by Cezary Kaliszyk
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
2009-12-02, by Cezary Kaliszyk
Fixed unlam for non-abstractions and updated list_induct_part proof.
2009-12-02, by Cezary Kaliszyk
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
2009-12-02, by Cezary Kaliszyk
The conversion approach works.
2009-12-02, by Cezary Kaliszyk
Trying a conversion based approach.
2009-12-02, by Cezary Kaliszyk
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
2009-12-02, by Cezary Kaliszyk
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
2009-12-02, by Cezary Kaliszyk
back in working state
2009-12-01, by Cezary Kaliszyk
clean
2009-12-01, by Cezary Kaliszyk
fixed previous commit
2009-12-01, by Christian Urban
fixed problems with FOCUS
2009-12-01, by Christian Urban
added a make_inst test
2009-12-01, by Christian Urban
Transformation of QUOT_TRUE assumption by any given function
2009-12-01, by Cezary Kaliszyk
QUOT_TRUE joke
2009-12-01, by Christian Urban
Removed last HOL_ss
2009-12-01, by Cezary Kaliszyk
more cleaning
2009-12-01, by Cezary Kaliszyk
Cleaning 'aps'.
2009-12-01, by Cezary Kaliszyk
merge
2009-11-30, by Cezary Kaliszyk
cleaned inj_regabs_trm
2009-11-30, by Christian Urban
merge
2009-11-30, by Cezary Kaliszyk
clean_tac rewrites the definitions the other way
2009-11-30, by Cezary Kaliszyk
merged
2009-11-30, by Christian Urban
added facilities to get all stored quotient data (equiv thms etc)
2009-11-30, by Christian Urban
More code cleaning
2009-11-30, by Cezary Kaliszyk
Code cleaning.
2009-11-30, by Cezary Kaliszyk
Commented clean-tac
2009-11-30, by Cezary Kaliszyk
Added another induction to LFex
2009-11-30, by Cezary Kaliszyk
tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29, by Christian Urban
added a new version of QuotMain to experiment with qids
2009-11-29, by Christian Urban
started functions for qid-insertion and fixed a bug in regularise
2009-11-29, by Christian Urban
Removed unnecessary HOL_ss which proved one of the subgoals.
2009-11-29, by Cezary Kaliszyk
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
2009-11-29, by Cezary Kaliszyk
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-29, by Christian Urban
tuned
2009-11-29, by Christian Urban
improved pattern matching inside the inj_repabs_tacs
2009-11-28, by Christian Urban
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
2009-11-28, by Christian Urban
removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28, by Christian Urban
renamed r_mk_comb_tac to inj_repabs_tac
2009-11-28, by Christian Urban
tuning
2009-11-28, by Christian Urban
tuned comments
2009-11-28, by Christian Urban
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
2009-11-28, by Christian Urban
Manually finished LF induction.
2009-11-28, by Cezary Kaliszyk
Moved fast instantiation to QuotMain
2009-11-28, by Cezary Kaliszyk
LFex proof a bit further.
2009-11-28, by Cezary Kaliszyk
merge
2009-11-28, by Cezary Kaliszyk
Looking at repabs proof in LF.
2009-11-28, by Cezary Kaliszyk
further proper merge
2009-11-28, by Christian Urban
merged
2009-11-28, by Christian Urban
more simplification
2009-11-28, by Christian Urban
Merged and tested that all works.
2009-11-28, by Cezary Kaliszyk
Finished and tested the new regularize
2009-11-28, by Cezary Kaliszyk
more tuning of the repabs-tactics
2009-11-28, by Christian Urban
fixed examples in IntEx and FSet
2009-11-28, by Christian Urban
merged
2009-11-28, by Christian Urban
fixed previous commit
2009-11-28, by Christian Urban
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28, by Cezary Kaliszyk
Merged comment
2009-11-28, by Cezary Kaliszyk
Integrated Stefan's tactic and changed substs to simps with empty context.
2009-11-28, by Cezary Kaliszyk
some slight tuning of the apply-tactic
2009-11-28, by Christian Urban
annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-28, by Christian Urban
Merge
2009-11-27, by Cezary Kaliszyk
The magical code from Stefan, will need to be integrated in the Simproc.
2009-11-27, by Cezary Kaliszyk
replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27, by Christian Urban
Simplifying arguments; got rid of trans2_thm.
2009-11-27, by Cezary Kaliszyk
Cleaning of LFex. Lambda_prs fails to unify in 2 places.
2009-11-27, by Cezary Kaliszyk
Recommit
2009-11-27, by Cezary Kaliszyk
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27, by Cezary Kaliszyk
More cleaning in QuotMain, identity handling.
2009-11-27, by Cezary Kaliszyk
Minor cleaning
2009-11-27, by Cezary Kaliszyk
tuned
2009-11-27, by Christian Urban
some tuning
2009-11-27, by Christian Urban
simplified gen_frees_tac and properly named abstracted variables
2009-11-27, by Christian Urban
removed CHANGED'
2009-11-27, by Christian Urban
introduced a separate lemma for id_simps
2009-11-27, by Christian Urban
renamed inj_REPABS to inj_repabs_trm
2009-11-27, by Christian Urban
tuned comments and moved slightly some code
2009-11-27, by Christian Urban
deleted obsolete qenv code
2009-11-27, by Christian Urban
renamed REGULARIZE to be regularize
2009-11-27, by Christian Urban
more tuning
2009-11-26, by Christian Urban
deleted get_fun_old and stuff
2009-11-26, by Christian Urban
recommited changes of comments
2009-11-26, by Christian Urban
Merge Again
2009-11-26, by Cezary Kaliszyk
Merged
2009-11-26, by Cezary Kaliszyk
tuned comments
2009-11-26, by Christian Urban
some diagnostic code for r_mk_comb
2009-11-26, by Christian Urban
introduced a new property for Ball and ===> on the left
2009-11-26, by Christian Urban
fixed QuotList
2009-11-26, by Christian Urban
changed left-res
2009-11-26, by Christian Urban
Manually regularized akind_aty_atrm.induct
2009-11-26, by Cezary Kaliszyk
Playing with Monos in LFex.
2009-11-26, by Cezary Kaliszyk
Fixed FSet after merge.
2009-11-26, by Cezary Kaliszyk
merged
2009-11-26, by Christian Urban
test with monos
2009-11-26, by Christian Urban
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
slight tuning
2009-11-21, by Christian Urban
some debugging code, but cannot find the place where the cprems_of exception is raised
2009-11-21, by Christian Urban
tried to prove the repabs_inj lemma, but failed for the moment
2009-11-21, by Christian Urban
my first version of repabs injection
2009-11-21, by Christian Urban
tuned
2009-11-21, by Christian Urban
tunded
2009-11-21, by Christian Urban
tuned
2009-11-21, by Christian Urban
flagged qenv-stuff as obsolete
2009-11-21, by Christian Urban
simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-21, by Christian Urban
started regularize of rtrm/qtrm version; looks quite promising
2009-11-20, by Christian Urban
updated to new Isabelle
2009-11-19, by Christian Urban
fixed the storage of qconst definitions
2009-11-18, by Christian Urban
Still don't know how to do the proof automatically.
2009-11-13, by Cezary Kaliszyk
added some tracing information to all phases of lifting to the function lift_thm
2009-11-13, by Christian Urban
merge of the merge?
2009-11-12, by Cezary Kaliszyk
merged
2009-11-12, by Cezary Kaliszyk
added a FIXME commment
2009-11-12, by Christian Urban
looking up data in quot_info works now (needs qualified string)
2009-11-12, by Christian Urban
changed the quotdata to be a symtab table (needs fixing)
2009-11-12, by Christian Urban
less
more
|
(0)
-240
+240
+1000
tip