| Fri, 10 Jan 2014 09:48:11 +0100 |
blanchet |
fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 16:40:50 +0100 |
blanchet |
reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 15:49:19 +0100 |
blanchet |
strengthened tactics w.r.t. 'lets' and tuples
|
file |
diff |
annotate
|
| Thu, 09 Jan 2014 15:08:24 +0100 |
blanchet |
strengthen tac w.r.t. lets with tuples
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 14:14:16 +0100 |
blanchet |
more SML-ish (less Haskell-ish) naming convention
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 14:04:37 +0100 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 13:55:34 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Fri, 03 Jan 2014 11:26:44 +0100 |
blanchet |
instantiate schematics as projections to avoid HOU trouble
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 23:07:49 +0100 |
blanchet |
generalized tactic to the case of several assumptions per equation
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 22:23:00 +0100 |
blanchet |
made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 21:35:21 +0100 |
blanchet |
made tactic more robust
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 20:51:09 +0100 |
blanchet |
made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 20:25:40 +0100 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 20:10:08 +0100 |
blanchet |
prevent tactic from getting out of sync and wrongly attack next subgoal
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
properly synchronize parallel lists
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
graceful handling of one-constructor case
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
gracefully handle single-equation case, where 'nchotomy' is 'True'
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
made tactic handle gracefully the case of missing constructors
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
don't generate any proof obligation for implicit (de facto) exclusiveness
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
generate 'disc_iff' property in 'primcorec'
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 09:50:22 +0100 |
blanchet |
added tactic to prove 'disc_iff' properties in 'primcorec'
|
file |
diff |
annotate
|
| Sat, 21 Dec 2013 09:44:30 +0100 |
blanchet |
generate exhaust from nchotomy
|
file |
diff |
annotate
|
| Sat, 21 Dec 2013 09:44:29 +0100 |
blanchet |
made tactic work with theorems with multiple assumptions
|
file |
diff |
annotate
|
| Sat, 21 Dec 2013 09:44:28 +0100 |
blanchet |
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 21:49:30 +0100 |
blanchet |
implemented 'exhaustive' option in tactic
|
file |
diff |
annotate
|
| Sun, 01 Dec 2013 19:32:57 +0100 |
panny |
more work towards "exhaustive"
|
file |
diff |
annotate
|
| Wed, 06 Nov 2013 13:00:45 +0100 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 16:53:43 +0100 |
blanchet |
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
|
file |
diff |
annotate
| base
|