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
|