--- a/src/HOLCF/IOA/meta_theory/TL.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Fri Mar 06 15:19:29 1998 +0100
@@ -138,7 +138,7 @@
val tsuffix_TL2 = conjI RS tsuffix_TL;
-
+Delsplits[expand_if];
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def]
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
auto();
@@ -152,6 +152,7 @@
by (REPEAT (atac 1));
auto();
qed"LTL1";
+Addsplits[expand_if];
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def]
@@ -188,4 +189,4 @@
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
goal thy "!! P. validT P ==> validT (Next P)";
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
-(* qed"NextTauto"; *)
\ No newline at end of file
+(* qed"NextTauto"; *)