--- a/src/HOLCF/Fun1.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/HOLCF/Fun1.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/fun1.ML
+(* Title: HOLCF/fun1.ML
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Lemmas for fun1.thy
@@ -14,30 +14,30 @@
qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun f f"
(fn prems =>
- [
- (fast_tac (HOL_cs addSIs [refl_less]) 1)
- ]);
+ [
+ (fast_tac (HOL_cs addSIs [refl_less]) 1)
+ ]);
qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def]
- "[|less_fun f1 f2; less_fun f2 f1|] ==> f1 = f2"
+ "[|less_fun f1 f2; less_fun f2 f1|] ==> f1 = f2"
(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (expand_fun_eq RS ssubst) 1),
- (fast_tac (HOL_cs addSIs [antisym_less]) 1)
- ]);
+ [
+ (cut_facts_tac prems 1),
+ (rtac (expand_fun_eq RS ssubst) 1),
+ (fast_tac (HOL_cs addSIs [antisym_less]) 1)
+ ]);
qed_goalw "trans_less_fun" Fun1.thy [less_fun_def]
- "[|less_fun f1 f2; less_fun f2 f3 |] ==> less_fun f1 f3"
+ "[|less_fun f1 f2; less_fun f2 f3 |] ==> less_fun f1 f3"
(fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (rtac trans_less 1),
- (etac allE 1),
- (atac 1),
- ((etac allE 1) THEN (atac 1))
- ]);
+ [
+ (cut_facts_tac prems 1),
+ (strip_tac 1),
+ (rtac trans_less 1),
+ (etac allE 1),
+ (atac 1),
+ ((etac allE 1) THEN (atac 1))
+ ]);
(*
--------------------------------------------------------------------------