isabelle: src/HOL/IMP/Denotation.ML@608483c2122a (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	1	(* Title: HOL/IMP/Denotation.ML
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	4	Copyright 1994 TUM
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	6
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	7	open Denotation;
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	9	(** Rewrite Rules for A,B,C **)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	10
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11	val B_simps = map (fn t => t RS eq_reflection)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	12	[B_true,B_false,B_op,B_not,B_and,B_or]
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	13
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	14	val C_simps = map (fn t => t RS eq_reflection)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	15	[C_skip,C_assign,C_comp,C_if,C_while];
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	16
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	17	(** mono (Gamma(b,c)) **)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	18
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	19	qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	20	"mono (Gamma b c)"
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	21	(fn _ => [(best_tac comp_cs 1)]);

author	clasohm
	Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476	608483c2122a
parent 1465	5d7a7e439cec
child 1481	03f096efa26d
permissions	-rw-r--r--