diff options
author | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 19:51:20 +0000 |
---|---|---|
committer | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 19:51:20 +0000 |
commit | 7e51746d8898e7c47e7804a52536e2ddefcbcbaf (patch) | |
tree | 0a51219f7c26543f87de9049df8ff7f98a838e20 /theories/Reals/SplitAbsolu.v | |
parent | cd9ccfffcfe7c8377babe72fd4177f490da4b684 (diff) |
Ajout tactics Reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1658 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/SplitAbsolu.v')
-rw-r--r-- | theories/Reals/SplitAbsolu.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v new file mode 100644 index 000000000..3b423aefb --- /dev/null +++ b/theories/Reals/SplitAbsolu.v @@ -0,0 +1,22 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +Require Export Rbasic_fun. + +Tactic Definition SplitAbs := + Match Context With + | [ |- [(case_Rabsolu ?1)] ] -> + Case (case_Rabsolu ?1); Try SplitAbs. + + +Tactic Definition SplitAbsolu := + Match Context With + | [ id:[(Rabsolu ?)] |- ? ] -> Generalize id; Clear id;Try SplitAbsolu + | [ |- [(Rabsolu ?1)] ] -> Unfold Rabsolu; Try SplitAbs;Intros. |