--- a/src/ZF/simpdata.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/simpdata.ML Tue Jan 30 13:42:57 1996 +0100
@@ -40,35 +40,35 @@
(*Analyse a theorem to atomic rewrite rules*)
fun atomize (conn_pairs, mem_pairs) th =
let fun tryrules pairs t =
- case head_of t of
- Const(a,_) =>
- (case assoc(pairs,a) of
- Some rls => flat (map (atomize (conn_pairs, mem_pairs))
- ([th] RL rls))
- | None => [th])
- | _ => [th]
+ case head_of t of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some rls => flat (map (atomize (conn_pairs, mem_pairs))
+ ([th] RL rls))
+ | None => [th])
+ | _ => [th]
in case concl_of th of
- Const("Trueprop",_) $ P =>
- (case P of
- Const("op :",_) $ a $ b => tryrules mem_pairs b
- | Const("True",_) => []
- | Const("False",_) => []
- | A => tryrules conn_pairs A)
+ Const("Trueprop",_) $ P =>
+ (case P of
+ Const("op :",_) $ a $ b => tryrules mem_pairs b
+ | Const("True",_) => []
+ | Const("False",_) => []
+ | A => tryrules conn_pairs A)
| _ => [th]
end;
(*Analyse a rigid formula*)
val ZF_conn_pairs =
- [("Ball", [bspec]),
- ("All", [spec]),
- ("op -->", [mp]),
- ("op &", [conjunct1,conjunct2])];
+ [("Ball", [bspec]),
+ ("All", [spec]),
+ ("op -->", [mp]),
+ ("op &", [conjunct1,conjunct2])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =
- [("Collect", [CollectD1,CollectD2]),
- ("op -", [DiffD1,DiffD2]),
- ("op Int", [IntD1,IntD2])];
+ [("Collect", [CollectD1,CollectD2]),
+ ("op -", [DiffD1,DiffD2]),
+ ("op Int", [IntD1,IntD2])];
val ZF_simps =
[empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
@@ -86,5 +86,5 @@
val ZF_ss = FOL_ss
setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
addsimps (ZF_simps @ mem_simps @ bquant_simps @
- Collect_simps @ UnInt_simps)
+ Collect_simps @ UnInt_simps)
addcongs ZF_congs;