author wenzelm Fri Jun 04 19:57:31 1999 +0200 (1999-06-04) changeset 6779 2912aff958bd parent 6778 2f66eea8a025 child 6780 769cea1985e4
Calculation.thy: Setup transitivity rules for calculational proofs.
 src/HOL/Calculation.thy file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Main.thy file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Calculation.thy	Fri Jun 04 19:57:31 1999 +0200
1.3 @@ -0,0 +1,23 @@
1.4 +(*  Title:      HOL/Calculation.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Markus Wenzel, TU Muenchen
1.7 +
1.8 +Setup transitivity rules for calculational proofs.
1.9 +*)
1.10 +
1.11 +theory Calculation = Int:
1.12 +
1.13 +
1.14 +theorems[trans] = HOL.trans			(*  =  =  =  *)
1.15 +theorems[trans] = HOL.ssubst                    (*  =  *  *  *)
1.16 +theorems[trans] = HOL.subst[COMP swap_prems_rl]	(*  *  =  *  *)
1.17 +
1.18 +theorems[trans] = Ord.order_trans		(*  <= <= <= *)
1.19 +theorems[trans] = Ord.order_less_trans		(*  <  <  <  *)
1.20 +theorems[trans] = Ord.order_le_less_trans	(*  <= <  <  *)
1.21 +theorems[trans] = Ord.order_less_le_trans	(*  <  <= <  *)
1.22 +
1.23 +theorems[trans] = Divides.dvd_trans		(* dvd dvd dvd *)
1.24 +
1.25 +
1.26 +end
```
```     2.1 --- a/src/HOL/IsaMakefile	Fri Jun 04 19:55:41 1999 +0200
2.2 +++ b/src/HOL/IsaMakefile	Fri Jun 04 19:57:31 1999 +0200
2.3 @@ -43,24 +43,24 @@
2.4    \$(SRC)/TFL/thms.sig \$(SRC)/TFL/thms.sml \$(SRC)/TFL/thry.sig \
2.5    \$(SRC)/TFL/thry.sml \$(SRC)/TFL/usyntax.sig \$(SRC)/TFL/usyntax.sml \
2.6    \$(SRC)/TFL/utils.sig \$(SRC)/TFL/utils.sml Arith.ML Arith.thy \
2.7 -  Datatype.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
2.8 -  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
2.9 -  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML \
2.10 -  Integ/IntDef.thy Integ/Int.ML Integ/Int.thy Integ/simproc.ML Lfp.ML \
2.11 -  Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy \
2.12 -  NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
2.13 -  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
2.14 -  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
2.15 -  String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
2.16 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
2.17 -  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
2.18 -  Tools/induct_method.ML Tools/inductive_package.ML \
2.19 -  Tools/primrec_package.ML Tools/recdef_package.ML \
2.20 -  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
2.21 -  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
2.22 -  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
2.23 -  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
2.24 -  thy_syntax.ML
2.25 +  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
2.26 +  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
2.27 +  Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
2.28 +  Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
2.29 +  Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
2.30 +  Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
2.31 +  Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML \
2.32 +  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
2.33 +  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
2.34 +  Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
2.35 +  Tools/datatype_package.ML Tools/datatype_prop.ML \
2.36 +  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
2.37 +  Tools/inductive_package.ML Tools/primrec_package.ML \
2.38 +  Tools/recdef_package.ML Tools/record_package.ML \
2.39 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
2.40 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
2.41 +  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
2.42 +  subset.ML subset.thy thy_syntax.ML
2.43  	@\$(ISATOOL) usedir -b \$(OUT)/Pure HOL
2.44
2.45
```
```     3.1 --- a/src/HOL/Main.thy	Fri Jun 04 19:55:41 1999 +0200
3.2 +++ b/src/HOL/Main.thy	Fri Jun 04 19:57:31 1999 +0200
3.3 @@ -1,4 +1,4 @@
3.4
3.5  (*theory Main includes everything*)
3.6
3.7 -Main = Bin + Map + Recdef + Record + RelPow + Sexp + String
3.8 +Main = Bin + Map + Recdef + Record + RelPow + Sexp + String + Calculation
```