src/CCL/Type.ML
changeset 5062 fbdb0b541314
parent 3837 d7f033c74b38
child 17456 bcf7544875b2
     1.1 --- a/src/CCL/Type.ML	Mon Jun 22 15:09:59 1998 +0200
     1.2 +++ b/src/CCL/Type.ML	Mon Jun 22 15:18:02 1998 +0200
     1.3 @@ -108,11 +108,11 @@
     1.4  
     1.5  (*** Monotonicity ***)
     1.6  
     1.7 -goal Type.thy "mono (%X. X)";
     1.8 +Goal "mono (%X. X)";
     1.9  by (REPEAT (ares_tac [monoI] 1));
    1.10  qed "idM";
    1.11  
    1.12 -goal Type.thy "mono(%X. A)";
    1.13 +Goal "mono(%X. A)";
    1.14  by (REPEAT (ares_tac [monoI,subset_refl] 1));
    1.15  qed "constM";
    1.16  
    1.17 @@ -156,18 +156,18 @@
    1.18  
    1.19  (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
    1.20  
    1.21 -goal Type.thy "mono(%X. Unit+X)";
    1.22 +Goal "mono(%X. Unit+X)";
    1.23  by (REPEAT (ares_tac [PlusM,constM,idM] 1));
    1.24  qed "NatM";
    1.25  bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
    1.26  
    1.27 -goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
    1.28 +Goal "mono(%X.(Unit+Sigma(A,%y. X)))";
    1.29  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    1.30  qed "ListM";
    1.31  bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
    1.32  bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
    1.33  
    1.34 -goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
    1.35 +Goal "mono(%X.({} + Sigma(A,%y. X)))";
    1.36  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    1.37  qed "IListsM";
    1.38  bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));