isabelle: src/HOL/Lex/AutoProj.ML@5c44de6aadf4 (annotated)

4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	1	(* Title: HOL/Lex/AutoProj.ML
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	2	ID: $Id$
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	3	Author: Tobias Nipkow
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	4	Copyright 1998 TUM
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	5	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	6
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4832 diff changeset	7	Goalw [start_def] "start(q,d,f) = q";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	8	by (Simp_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	9	qed "start_conv";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	10
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4832 diff changeset	11	Goalw [next_def] "next(q,d,f) = d";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	12	by (Simp_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	13	qed "next_conv";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	14
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4832 diff changeset	15	Goalw [fin_def] "fin(q,d,f) = f";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	16	by (Simp_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	17	qed "fin_conv";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	18
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19	Addsimps [start_conv,next_conv,fin_conv];

author	paulson
	Mon, 18 Dec 2000 12:21:54 +0100
changeset 10689	5c44de6aadf4
parent 5132	24f992a25adc
permissions	-rw-r--r--