# HG changeset patch
# User lcp
# Date 783614143 -3600
# Node ID 7fe6ec24d84293c9baeb44e4da1a4206907e4d34
# Parent  95ed2ccb443810c9adff5851cd62703f066976a3
added header files; deleted commented-out code

diff -r 95ed2ccb4438 -r 7fe6ec24d842 src/LCF/fix.ML
--- a/src/LCF/fix.ML	Fri Oct 28 10:13:16 1994 +0100
+++ b/src/LCF/fix.ML	Mon Oct 31 15:35:43 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title: 	LCF/fix
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1992  University of Cambridge
+
+Fixedpoint theory
+*)
+
 signature FIX =
 sig
   val adm_eq: thm
@@ -25,18 +33,18 @@
 val tac = rtac tr_induct 1 THEN REPEAT(simp_tac LCF_ss 1);
 
 val not_eq_TT = prove_goal LCF.thy "ALL p. ~p=TT <-> (p=FF | p=UU)"
-	(fn _ => [tac]) RS spec;
+    (fn _ => [tac]) RS spec;
 
 val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <-> (p=TT | p=UU)"
-	(fn _ => [tac]) RS spec;
+    (fn _ => [tac]) RS spec;
 
 val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
-	(fn _ => [tac]) RS spec;
+    (fn _ => [tac]) RS spec;
 
 val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)"
-	(fn _ => [rtac tr_induct 1,
-	REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
-               REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
+    (fn _ => [rtac tr_induct 1,
+    REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
+	   REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
 
 val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr,
 		  adm_conj,adm_disj,adm_imp,adm_all];
@@ -59,22 +67,6 @@
 val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq;
 val ss = LCF_ss addsimps [ffix,gfix];
 
-(* Do not use prove_goal because the result is ?ed which leads to divergence
-   when submitted as an argument to SIMP_THM *)
-(*
-local
-val thm = trivial(read_cterm(sign_of LCF.thy)
-        ("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT));
-val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss,
-	  strip_tac, simp_tac (LCF_ss addsimps [PROD_less]),
-	  rtac conjI, rtac least_FIX, etac subst, rtac (FST RS sym),
-	  rtac least_FIX, etac subst, rtac (SND RS sym)];
-in
-val Some(FIX_pair,_) = Sequence.pull(tapply(tac,thm));
-end;
-
-val FIX_pair_conj = SIMP_THM (LCF_ss addsimps [PROD_eq]) FIX_pair;
-*)
 val FIX_pair = prove_goal LCF.thy
   "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
   (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1,
diff -r 95ed2ccb4438 -r 7fe6ec24d842 src/LCF/pair.ML
--- a/src/LCF/pair.ML	Fri Oct 28 10:13:16 1994 +0100
+++ b/src/LCF/pair.ML	Mon Oct 31 15:35:43 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title: 	LCF/pair
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1992  University of Cambridge
+
+Theory of ordered pairs and products
+*)
+
 val expand_all_PROD = prove_goal LCF.thy
 	"(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
 	(fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1,