src/LCF/ex/Ex3.ML
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 5061 f947332d5465
child 17248 81bf91654e73
permissions -rw-r--r--
added HOL/Prolog
     1 
     2 simpset_ref() := LCF_ss;
     3 
     4 Addsimps [p_strict,p_s];
     5 
     6 Goal "p(FIX(s),y) = FIX(s)";
     7 by (induct_tac "s" 1);
     8 by (Simp_tac 1);
     9 by (Simp_tac 1);
    10 qed "example";
    11