--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Examples.ML Tue Jul 04 14:04:56 2000 +0200
@@ -0,0 +1,45 @@
+(* Title: HOL/IMP/Examples.ML
+ ID: $Id$
+ Author: David von Oheimb, TUM
+ Copyright 2000 TUM
+*)
+
+(*###should go to Fun.ML*)
+Goal "f(x:=y,a:=b,x:=z) = f(a:=b,x:=z)";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "fun_upd_upd2";
+Addsimps [fun_upd_upd2];
+
+Addsimps[update_def];
+
+section "Examples";
+
+val step = resolve_tac evalc.intrs 1;
+val simp = Asm_simp_tac 1;
+Goalw [factorial_def] "a~=b ==> \
+\ <factorial a b, Mem(a:=#3)> -c-> Mem(b:=#6,a:=#0)";
+by (ftac not_sym 1);
+by step;
+by step;
+by step;
+by simp;
+by step;
+by step;
+by step;
+by simp;
+by step;
+by simp;
+by step;
+by step;
+by step;
+by simp;
+by step;
+by simp;
+by step;
+by step;
+by step;
+by simp;
+by step;
+by simp;
+qed "factorial_3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Examples.thy Tue Jul 04 14:04:56 2000 +0200
@@ -0,0 +1,20 @@
+(* Title: HOL/IMP/Examples.thy
+ ID: $Id$
+ Author: David von Oheimb, TUM
+ Copyright 2000 TUM
+*)
+
+Examples = Natural +
+
+defs (* bring up the deferred definition for update *)
+
+ update_def "update == fun_upd"
+
+constdefs
+
+ factorial :: loc => loc => com
+ "factorial a b == b :== (%s. 1);
+ WHILE (%s. s a ~= 0) DO
+ (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+
+end